proposition: Lemma app_conv : forall M N (Mapp: isApp M) (Napp: isApp N) Q, (appBodyL Mapp) ~(Q) (appBodyL Napp) -> (appBodyR Mapp) ~(Q) (appBodyR Napp) -> M ~(Q) N.
proof: Proof. intros. term_inv M; term_inv N. destruct H; destruct H0. assert (Conv_term: conv_term (term Tr) (term Tr0) Q). simpl; constructor 4; trivial. constructor; trivial. apply conv_env_app with I I; simpl; trivial. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)