Theorem: MvQPF.Cofix.bisim_rel (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 y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.30288 r x y = ?m.30290 r x y
⊢ ∀ (x y : sorryAx (Type u_3) true), r x y → x = y
Tactic:
let r' (x y) := x = y ∨ r x y
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 y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.30288 r x y = ?m.30290 r x y
r' : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop := fun x y => x = y ∨ r x y
⊢ ∀ (x 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 y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.30288 r x y = ?m.30290 r x y
r' : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop := fun x y => x = y ∨ r x y
⊢ ∀ (x y : sorryAx (Type u_3) true), r x y → x = y
Tactic:
intro x y rxy
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 y : sorryAx (Type u_3) true), r x y → (TypeVec.id ::: Quot.mk r) <$$> ?m.30288 r x y = ?m.30290 r x y
r' : sorryAx (Type u_3) true → sorryAx (Type u_3) true → Prop := fun x y => x = y ∨ r x y
x y : sorryAx (Type u_3) true
rxy : r x y
⊢ x = y