constructor
case mpr.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos S a✝ a✝
no goals