apply both_inclusions <;> intros x y hyp
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 R)) (trans_clos (refl_clos R))
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : refl_clos (trans_clos R) x y
⊢ trans_clos (refl_clos R) x y

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