proposition: Lemma Crel_strext_imp_lftarg : Crel_strext -> Crel_strext_lft.
proof: Proof. intros H x1 x2 y H0. generalize (H x1 x2 y y). 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