diff --git a/tests/lean/run/adamTC.lean b/tests/lean/run/adamTC.lean
new file mode 100644
index 0000000000..0b97d646b4
--- /dev/null
+++ b/tests/lean/run/adamTC.lean
@@ -0,0 +1,63 @@
+inductive Expr where
+  | nat  : Nat → Expr
+  | plus : Expr → Expr → Expr
+  | bool : Bool → Expr
+  | and  : Expr → Expr → Expr
+  deriving DecidableEq
+
+inductive Ty where
+  | nat
+  | bool
+  deriving DecidableEq
+
+inductive HasType : Expr → Ty → Prop
+  | nat  : HasType (.nat v) .nat
+  | plus : HasType a .nat → HasType b .nat → HasType (.plus a b) .nat
+  | bool : HasType (.bool v) .bool
+  | and  : HasType a .bool → HasType b .bool → HasType (.and a b) .bool
+
+def Expr.typeCheck (e : Expr) : Option {t : Ty // HasType e t} :=
+  match e with
+  | nat ..   => some ⟨.nat, .nat⟩
+  | bool ..  => some ⟨.bool, .bool⟩
+  | plus a b =>
+    match a.typeCheck, b.typeCheck with
+    | some ⟨.nat, h₁⟩, some ⟨.nat, h₂⟩ => some ⟨.nat, .plus h₁ h₂⟩
+    | _, _ => none
+  | and a b =>
+    match a.typeCheck, b.typeCheck with
+    | some ⟨.bool, h₁⟩, some ⟨.bool, h₂⟩ => some ⟨.bool, .and h₁ h₂⟩
+    | _, _ => none
+
+theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
+  cases h₁ <;> cases h₂ <;> rfl
+
+-- TODO: for simplifying the following proof we need: ematching for forward reasoning, and `match` blast for case analysis
+
+theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = none → ¬ HasType e t := by
+  induction e with simp [typeCheck]
+  | plus a b iha ihb =>
+    revert iha ihb
+    cases typeCheck a <;> cases typeCheck b <;> simp <;> intros <;> intro h <;> cases h <;> try contradiction
+    rename_i r₁ r₂ h _ _
+    cases r₁; rename_i t₁ _; cases r₂; rename_i t₂ _; cases t₁ <;> cases t₂ <;> simp at h
+    . have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction
+    . have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction
+    . have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction
+  | and a b iha ihb =>
+    revert iha ihb
+    cases typeCheck a <;> cases typeCheck b <;> simp <;> intros <;> intro h <;> cases h <;> try contradiction
+    rename_i r₁ r₂ h _ _
+    cases r₁; rename_i t₁ _; cases r₂; rename_i t₂ _; cases t₁ <;> cases t₂ <;> simp at h
+    . have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction
+    . have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction
+    . have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction
+
+instance (e : Expr) (t : Ty) : Decidable (HasType e t) :=
+  match h' : e.typeCheck with
+  | some ⟨t', ht'⟩ =>
+    if heq : t = t' then
+      isTrue (heq ▸ ht')
+    else
+      isFalse fun ht => heq (HasType.det ht ht')
+  | none => isFalse (Expr.typeCheck_complete h')
diff --git a/tests/lean/run/adamTC2.lean b/tests/lean/run/adamTC2.lean
new file mode 100644
index 0000000000..92690c78d4
--- /dev/null
+++ b/tests/lean/run/adamTC2.lean
@@ -0,0 +1,68 @@
+inductive Expr where
+  | nat  : Nat → Expr
+  | plus : Expr → Expr → Expr
+  | bool : Bool → Expr
+  | and  : Expr → Expr → Expr
+
+inductive Ty where
+  | nat
+  | bool
+  deriving DecidableEq
+
+inductive HasType : Expr → Ty → Prop
+  | nat  : HasType (.nat v) .nat
+  | plus : HasType a .nat → HasType b .nat → HasType (.plus a b) .nat
+  | bool : HasType (.bool v) .bool
+  | and  : HasType a .bool → HasType b .bool → HasType (.and a b) .bool
+
+inductive Maybe (p : α → Prop) where
+  | unknown
+  | found : (a : α) → p a → Maybe p
+
+notation "{{ " x " | " p " }}" => Maybe (fun x => p)
+
+def Expr.typeCheck (e : Expr) : {{ ty | HasType e ty }} :=
+  match e with
+  | nat ..   => .found .nat .nat
+  | bool ..  => .found .bool .bool
+  | plus a b =>
+    match a.typeCheck, b.typeCheck with
+    | .found .nat h₁, .found .nat h₂ => .found .nat (.plus h₁ h₂)
+    | _, _ => .unknown
+  | and a b =>
+    match a.typeCheck, b.typeCheck with
+    | .found .bool h₁, .found .bool h₂ => .found .bool (.and h₁ h₂)
+    | _, _ => .unknown
+
+theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := by
+  cases h₁ <;> cases h₂ <;> rfl
+
+-- TODO: for simplifying the following proof we need: ematching for forward reasoning, and `match` blast for case analysis
+
+theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e t := by
+  induction e with simp [typeCheck]
+  | plus a b iha ihb =>
+    revert iha ihb
+    cases typeCheck a <;> cases typeCheck b <;> simp <;> intros <;> intro h <;> cases h <;> try contradiction
+    rename_i ty₁ _ ty₂ _ h _ _
+    cases ty₁ <;> cases ty₂ <;> simp at h
+    . have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction
+    . have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction
+    . have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction
+  | and a b iha ihb =>
+    revert iha ihb
+    cases typeCheck a <;> cases typeCheck b <;> simp <;> intros <;> intro h <;> cases h <;> try contradiction
+    rename_i ty₁ _ ty₂ _ h _ _
+    cases ty₁ <;> cases ty₂ <;> simp at h
+    . have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction
+    . have := HasType.det ‹HasType a Ty.bool› ‹HasType a Ty.nat›; contradiction
+    . have := HasType.det ‹HasType b Ty.bool› ‹HasType b Ty.nat›; contradiction
+
+instance (e : Expr) (t : Ty) : Decidable (HasType e t) :=
+  match h' : e.typeCheck with
+  | .found t' ht' =>
+    if heq : t = t' then
+      isTrue (heq ▸ ht')
+    else
+      isFalse fun ht => heq (HasType.det ht ht')
+  | .unknown => isFalse (Expr.typeCheck_complete h')