proposition: Lemma partialFlattening_subterm_aux : forall N L M, L <> nil -> appUnits M ++ L = appUnits N -> subterm M N.
proof: Proof. intro N. apply well_founded_ind with (R := subterm) (P := fun N => forall L M, L <> nil -> appUnits M ++ L = appUnits N -> subterm M N ). apply subterm_wf. clear N; intros N IH L M L_neq_nil units. destruct L. tauto. case (isApp_dec N). intro Napp. rewrite (appUnits_app N Napp) in units; trivial. constructor 1 with Napp. destruct L. assert (Meq: M = appBodyL Napp). destruct (app_inj_tail (appUnits M) (appUnits (appBodyL Napp)) t (appBodyR Napp)) as [unitsEq _]; trivial. apply eq_units_eq_terms; trivial. rewrite Meq; constructor 2. rewrite <- list_app_first_last in units. destruct (@list_drop_last Term (appUnits M ++ t::nil) (t0::L) (appUnits (appBodyL Napp)) (appBodyR Napp)); auto with datatypes. constructor 1. apply IH with (t::x); auto with datatypes. constructor 1 with Napp; constructor 2. rewrite <- list_app_first_last; trivial. intro Nnapp. rewrite (appUnits_notApp N) in units; trivial. exfalso; eapply appUnits_notEmpty; eexact units. Qed.
imports: CoLoR(RelExtras ListExtras TermsTyping LogicUtil) Coq(Lia)