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