Qed.
Lemma Crel_strextarg_imp_strext :
Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
intros H H0 x1 x2 y1 y2 H1.
Qed.
Lemma Crel_strextarg_imp_strext :
Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
intros H H0 x1 x2 y1 y2 H1.