Theorem: MvQPF.Cofix.bisim_aux (Qpf/Qpf/Multivariate/Constructions/Cofix.lean)

State before:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h' : ∀ (x : sorryAx (Type u_3) true), r x x
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.27762 r h' x y = ?m.27766 r h' x y
⊢ ∀ (x y : sorryAx (Type u_3) true), r x y → x = y
Tactic:
intro x
State after:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h' : ∀ (x : sorryAx (Type u_3) true), r x x
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.27762 r h' x y = ?m.27766 r h' x y
x : sorryAx (Type u_3) true
⊢ ∀ (y : sorryAx (Type u_3) true), r x y → x = y

State before:
n : ℕ
x✝ : Sort u_1
Cofix : x✝
α : TypeVec.{u_2} n
r : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop
h' : ∀ (x : sorryAx (Type u_3) true), r x x
h : ∀ (x y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.27762 r h' x y = ?m.27766 r h' x y
x : sorryAx (Type u_3) true
⊢ ∀ (y : sorryAx (Type u_3) true), r x y → x = y
Tactic:
rcases x
State after:
no goals