proposition: Lemma beta_conv_comp : forall M M' N N' Q, M ~(Q) M' -> N ~(Q) N' -> M -b-> N -> env M' = env N' -> M' -b-> N'.
proof: Proof. intros. unfold BetaReduction. apply red_conv_comp with M N Q; trivial. intros. apply betaStep_conv_comp_aux with M0 N0 Q0; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsRed TermsConv LogicUtil) Coq(Setoid PeanoNat Lia)