proposition: Lemma rel_strextarg_imp_strext : rel_strext_rht -> rel_strext_lft -> rel_strext.
proof: Proof. intros H H0 x1 x2 y1 y2 H1. elim (H x1 y1 y2 H1); intro H2;[|elim (H0 x1 x2 y2 H2)];auto. Qed.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid