proposition: Lemma subst_conv_sym G1 G2 S : G1 ~~(S) G2 -> G2 ~~(envSubst_transp S) G1.
proof: Proof. intro G1G2. constructor; intros. destruct (@sc_rl G1 G2 S G1G2 y x T) as [T' [G1T' TT']]; trivial. destruct S; trivial. exists T'; split; auto. apply terms_conv_sym_aux; trivial. destruct (@sc_lr G1 G2 S G1G2 y x T') as [T [G2T' TT']]; trivial. destruct S; trivial. exists T; split; auto. apply terms_conv_sym_aux; trivial. destruct (sc_inj_r G1G2 H). exists x0; destruct S; trivial. destruct (sc_inj_l G1G2 H). exists x; destruct S; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)