Theorem: LoVe.Star_Star_Eq_Star (LoVe/Lectures/LoVe06_InductivePredicates_Demo.lean)

State before:
α : Type
R : α → α → Prop
⊢ Star (Star R) = Star R
Tactic:
apply funext
State after:
case h
α : Type
R : α → α → Prop
⊢ ∀ (x : α), Star (Star R) x = Star R x

State before:
case h
α : Type
R : α → α → Prop
⊢ ∀ (x : α), Star (Star R) x = Star R x
Tactic:
intro a
State after:
case h
α : Type
R : α → α → Prop
a : α
⊢ Star (Star R) a = Star R a

State before:
case h
α : Type
R : α → α → Prop
a : α
⊢ Star (Star R) a = Star R a
Tactic:
apply funext
State after:
case h.h
α : Type
R : α → α → Prop
a : α
⊢ ∀ (x : α), Star (Star R) a x = Star R a x

State before:
case h.h
α : Type
R : α → α → Prop
a : α
⊢ ∀ (x : α), Star (Star R) a x = Star R a x
Tactic:
intro b
State after:
case h.h
α : Type
R : α → α → Prop
a b : α
⊢ Star (Star R) a b = Star R a b

State before:
case h.h
α : Type
R : α → α → Prop
a b : α
⊢ Star (Star R) a b = Star R a b
Tactic:
apply propext
State after:
case h.h.a
α : Type
R : α → α → Prop
a b : α
⊢ Star (Star R) a b ↔ Star R a b

State before:
case h.h.a
α : Type
R : α → α → Prop
a b : α
⊢ Star (Star R) a b ↔ Star R a b
Tactic:
apply Star_Star_Iff_Star
State after:
no goals