proposition: Lemma rel_strext_imp_lftarg : rel_strext -> rel_strext_lft.
proof: Proof. intros H x1 x2 y H0. generalize (H x1 x2 y y). intros H1. elim (H1 H0);[|auto]. intros [H2|H3];[auto|]. elim (ap_irreflexive S _ H3). Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid