apply both_inclusions <;> intros
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (refl_clos (trans_clos (sym_clos R))) (trans_clos (sym_clos (refl_clos R)))
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (sym_clos (refl_clos R)) x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : trans_clos (sym_clos (refl_clos R)) x✝ y✝
⊢ refl_clos (trans_clos (sym_clos R)) x✝ y✝