proposition: Lemma betaStep_conv_comp_aux : forall M M' N N' Q, M ~(Q) M' -> N ~(Q) N' -> BetaStep M N -> env M' = env N' -> BetaStep M' N'.
proof: Proof. intros M M' N N' Q MQM' NQN' MN M'N'env. inversion MN. assert (M'app: isApp M'). assert (MM' : M ~ M') by (exists Q; trivial). rewrite <- MM'; trivial. assert (M'Labs: isAbs (appBodyL M'app)). setoid_replace (appBodyL M'app) with (appBodyL Mapp0); trivial. apply app_conv_app_left. sym; exists Q; trivial. replace N' with (lower (subst (beta_subst M' M'app M'Labs)) (beta_lowering M' M'app M'Labs)). constructor. rewrite terms_lift_eq with (lower (subst (beta_subst M' M'app M'Labs)) (beta_lowering M' M'app M'Labs)) N'; trivial. apply term_eq. autorewrite with terms datatypes using unfold liftedEnv, loweredEnv; simpl. rewrite M'N'env; trivial. rewrite prelift_prelower. autorewrite with terms. rewrite <- lift_term. apply (@presubst_singleton_conv_sim (term (absBody MLabs)) (term (absBody M'Labs)) (lift (appBodyR Mapp0) 1) (lift (appBodyR M'app) 1) (envSubst_lift1 Q) (term (lift N 1)) (term (lift N' 1)) ). destruct Q; simpl; trivial. assert (Conv: (absBody MLabs) ~(envSubst_lift1 Q) (absBody M'Labs)). apply abs_conv_absBody_aux. apply app_conv_app_left_aux; trivial. destruct Conv; trivial. apply terms_conv_conv_lift. apply app_conv_app_right_aux; trivial. assert (Conv: (lift N 1) ~(envSubst_lift1 Q) (lift N' 1)). apply terms_conv_conv_lift; trivial. destruct Conv; trivial. rewrite <- H0. rewrite prelift_prelower. autorewrite with terms using trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)