proposition: Lemma rel_strext_imp_rhtarg : rel_strext -> rel_strext_rht.
proof: Proof. intros H x y1 y2 H0. generalize (H x x y1 y2 H0). intros [[H1|H2]|H3]; auto. elim (ap_irreflexive _ _ H1). Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid