proposition: Lemma appHead_conv : forall M N Q, M ~(Q) N -> (appHead M) ~(Q) (appHead N).
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall N Q, M ~(Q) N -> (appHead M) ~(Q) (appHead N)). apply subterm_wf. clear M; intros M IH N Q MN. destruct (isApp_dec M). term_inv M. inversion MN. term_inv N; inversion H. rewrite appHead_app with Tr I. rewrite appHead_app with Tr0 I. apply IH. apply appBodyL_subterm. constructor; trivial. apply conv_env_appBodyL; trivial. rewrite appHead_notApp; trivial. rewrite appHead_notApp; trivial. term_inv N. inversion MN; inversion H; term_inv M. Qed.
imports: CoLoR(RelExtras ListPermutation TermsPos ListUtil ListExtras LogicUtil) Coq(Compare_dec Setoid Morphisms Lia PeanoNat)