proposition: Lemma conv_subst_conv_term_aux : forall M M' G G' Q, conv_term M M' Q -> G ~~(Q) G' -> conv_term (presubst M G) (presubst M' G') Q.
proof: Proof. induction M; intros; inversion H. unfold presubst; simpl. destruct (varSubst_dec G x) as [[T GxT] | GxN]. rewrite GxT. destruct (sc_lr H0 y H2 GxT) as [T' [G'yT' TT']]. rewrite G'yT'. rewrite !lift_0. destruct TT'; trivial. inversion GxN; rewrite H5; destruct (conv_subst_udecl y H0 H2 GxN); rewrite H6; constructor; trivial. unfold presubst; simpl; constructor. unfold presubst; simpl; constructor. set (w := subst_lift_subst_aux M (None::G) 0 1). simpl in w; rewrite w. set (w' := subst_lift_subst_aux R (None::G') 0 1). simpl in w'; rewrite w'. fold (presubst M (None::lift_subst G 1)). fold (presubst R (None::lift_subst G' 1)). apply IHM; trivial. apply subst_conv_cons; trivial. unfold presubst; simpl; constructor. fold (presubst M1 G); fold (presubst RL G'). apply IHM1; trivial. fold (presubst M2 G); fold (presubst RR G'). apply IHM2; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubst) Coq(Arith Lia)