proposition: Lemma compTerms : forall M N Ns, M [>>] Ns -> CompTerms (appArgs M) -> (forall n, In n Ns -> subterm n N) -> (forall N', subterm N' N -> M >> N' -> CompH N') -> CompTerms Ns.
proof: Proof. intros M N Ns M_red_Ns argsMcomp Ns_sub_N IH. induction M_red_Ns as [ M | M Th Tt M_red_Th M_red_Tt IHargs | M Th Tt Marg_red_Th M_red_Tt IHargs ]; unfold CompTerms. intros x in_x_nil; absurd (In x nil); auto. intros x x_Th_Tt; case x_Th_Tt; intro xT. rewrite <- xT. apply IH. apply Ns_sub_N; auto with datatypes. trivial. fold (In x Tt) in xT; apply IHargs; auto with datatypes. intros x x_Th_Tt; case x_Th_Tt; intro xT. rewrite <- xT. destruct Marg_red_Th as [M' M'arg M'_red_Th]. destruct M'_red_Th as [M' Th M_red_Th | M']. unfold CompH; apply horpo_comp_step_comp with M'. apply argsMcomp; trivial. trivial. apply argsMcomp; trivial. fold (In x Tt) in xT; apply IHargs; auto with datatypes. Qed.
imports: CoLoR(RelExtras ListExtras Horpo Computability PairLex HorpoComp LogicUtil)