theory Scratch
  imports Main
begin

class a = assumes a: "\<And>(x::'a) y. x \<noteq> y"
class b = assumes b: "\<And>(x::'a) y. x \<noteq> y"

instance a \<subseteq> b sorry


lemma
  assumes "SORT_CONSTRAINT('a::a)" "SORT_CONSTRAINT('b::b)"
  shows 1: "False \<and> False"
  apply (rule conjI)
  subgoal using a [where 'a = 'a] by auto
  subgoal using b [where 'a = 'b] by auto
  done

thm_deps 1  \<comment> \<open>uses @{thm classrel_a_b}\<close>
thm_oracles 1  \<comment> \<open>uses \<^ML>\<open>\<^oracle_name>\<open>skip_proof\<close>\<close>\<close>


lemma
  assumes "SORT_CONSTRAINT('a::{a,b})"  \<comment> \<open>normalized to \<^typ>\<open>'a::a\<close> in abstract syntax!\<close>
  shows 2: "False"
  using a [where 'a = 'a] by auto

thm_deps 2  \<comment> \<open>no @{thm classrel_a_b}\<close>
thm_oracles 2  \<comment> \<open>no \<^ML>\<open>\<^oracle_name>\<open>skip_proof\<close>\<close>\<close>

end