proposition: Lemma red_conv_comp : forall M N, Red M N -> forall M' N' Q, M ~(Q) M' -> N ~(Q) N' -> env M' = env N' -> Red M' N'.
proof: Proof. induction 1; intros. constructor. apply R_conv_comp with M N Q; trivial. assert (M'app: isApp M'). assert (H'1 : M ~ M') by (exists Q; trivial). rewrite <- H'1; trivial. assert (N'app: isApp N'). assert (H'2 : N ~ N') by (exists Q; trivial). rewrite <- H'2; trivial. constructor 2 with M'app N'app; trivial. apply IHReduction with Q. apply app_conv_app_left_aux; trivial. apply app_conv_app_left_aux; trivial. autorewrite with terms using trivial. apply term_eq. autorewrite with terms using trivial. apply conv_term_unique with (term (appBodyR Mapp)) Q. destruct (app_conv_app_right_aux Mapp M'app H1); trivial. rewrite H0. destruct (app_conv_app_right_aux Napp N'app H2); trivial. assert (M'app: isApp M'). assert (H'1 : M ~ M') by (exists Q; trivial). rewrite <- H'1; trivial. assert (N'app: isApp N'). assert (H'2 : N ~ N') by (exists Q; trivial). rewrite <- H'2; trivial. constructor 3 with M'app N'app; trivial. apply IHReduction with Q. apply app_conv_app_right_aux; trivial. apply app_conv_app_right_aux; trivial. autorewrite with terms using trivial. apply term_eq. autorewrite with terms using trivial. apply conv_term_unique with (term (appBodyL Mapp)) Q. destruct (app_conv_app_left_aux Mapp M'app H1); trivial. rewrite H0. destruct (app_conv_app_left_aux Napp N'app H2); trivial. assert (M'abs: isAbs M'). assert (H'1 : M ~ M') by (exists Q; trivial). rewrite <- H'1; trivial. assert (N'abs: isAbs N'). assert (H'2 : N ~ N') by (exists Q; trivial). rewrite <- H'2; trivial. assert (absType M'abs = absType N'abs). rewrite <- abs_conv_absType with M M' Mabs M'abs. rewrite <- abs_conv_absType with N N' Nabs N'abs. trivial. exists Q; trivial. exists Q; trivial. constructor 4 with M'abs N'abs; trivial. apply IHReduction with (envSubst_lift1 Q). apply abs_conv_absBody_aux; trivial. apply abs_conv_absBody_aux; trivial. autorewrite with terms. congruence. Qed.
imports: CoLoR(RelExtras ListExtras TermsSubstConv)