Theorem: red_ref_trans_clos (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (x y z : A), R x y → refl_trans_clos R y z → refl_trans_clos R x z
Tactic:
intros x y z red_x_y h
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
h : refl_trans_clos R y z
⊢ refl_trans_clos R x z

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
h : refl_trans_clos R y z
⊢ refl_trans_clos R x z
Tactic:
apply refl_trans_clos.step _ _ <;> trivial
State after:
no goals