α : Type u_1
β : Type ?u.16745
γ : Type ?u.16748
δ : Type ?u.16751
r : α → α → Prop
a b c d : α
h✝ : Symmetric r
x y : α
h : ReflTransGen r x y
⊢ ReflTransGen r y x
α : Type u_1
β : Type ?u.16745
γ : Type ?u.16748
δ : Type ?u.16751
r : α → α → Prop
a b c d : α
h : Symmetric r
⊢ Symmetric (ReflTransGen r)
intro x y h
case refl
α : Type u_1
β : Type ?u.16745
γ : Type ?u.16748
δ : Type ?u.16751
r : α → α → Prop
a b c d : α
h : Symmetric r
x y : α
⊢ ReflTransGen r x x

case tail
α : Type u_1
β : Type ?u.16745
γ : Type ?u.16748
δ : Type ?u.16751
r : α → α → Prop
a b✝ c✝ d : α
h : Symmetric r
x y z w : α
a✝ : ReflTransGen r x z
b : r z w
c : ReflTransGen r z x
⊢ ReflTransGen r w x
α : Type u_1
β : Type ?u.16745
γ : Type ?u.16748
δ : Type ?u.16751
r : α → α → Prop
a b c d : α
h✝ : Symmetric r
x y : α
h : ReflTransGen r x y
⊢ ReflTransGen r y x
induction' h with z w _ b c
no goals
case refl
α : Type u_1
β : Type ?u.16745
γ : Type ?u.16748
δ : Type ?u.16751
r : α → α → Prop
a b c d : α
h : Symmetric r
x y : α
⊢ ReflTransGen r x x
rfl
no goals
case tail
α : Type u_1
β : Type ?u.16745
γ : Type ?u.16748
δ : Type ?u.16751
r : α → α → Prop
a b✝ c✝ d : α
h : Symmetric r
x y z w : α
a✝ : ReflTransGen r x z
b : r z w
c : ReflTransGen r z x
⊢ ReflTransGen r w x
apply Relation.ReflTransGen.head (h b) c