α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ LiftRel (fun x x_1 => x = x_1) (think s) s
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ think s ~ʷ s
unfold Equiv
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ LiftRel (fun x x_1 => x = x_1) s s
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ LiftRel (fun x x_1 => x = x_1) (think s) s
simp
no goals
α : Type u
β : Type v
γ : Type w
s : WSeq α
⊢ LiftRel (fun x x_1 => x = x_1) s s
apply Equiv.refl