proposition: Lemma Crel_strextarg_imp_strext : Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
proof: Proof. intros H H0 x1 x2 y1 y2 H1. elim (H x1 y1 y2 H1); auto. intro H2. elim (H0 x1 x2 y2 H2); auto. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid