proposition: Lemma projection_is_subterm : forall t f l, Rdp0 (Term f l) t -> (match F.arity f with | AC => length l = 2 | C => length l = 2 | Free n => length l = n end) -> direct_subterm (projection (Term f l)) (Term f l).
proof: Proof. intros s f l K L. inversion K as [g l1 l2 t3 H1 H2]; subst. inversion H2 as [t1 t2 sigma K1 K2 K3]; subst. destruct t1 as [x | g1 k1]. inversion K1 as [J1 J2]; clear K K1 H2; subst. assert (K4 := cdp_in_dpR _ _ cdp_uv0). destruct K4 as [K4 _]; inversion K4. inversion K1 as [J1 J2]. rewrite J1 in P_ok; injection K2; clear K2; do 2 intro; subst. destruct (F.arity f) as [ | | n]. destruct k1 as [ | u1 [ | u2 [ | u3 l]]]; try discriminate. simpl; destruct (P f) as [ | [ | p]]; simpl. left; reflexivity. right; left; reflexivity. assert (Abs := le_S_n _ _ (le_S_n _ _ P_ok)); inversion Abs. destruct k1 as [ | u1 [ | u2 [ | u3 l]]]; try discriminate. simpl; destruct (P f) as [ | [ | p]]; simpl. left; reflexivity. right; left; reflexivity. assert (Abs := le_S_n _ _ (le_S_n _ _ P_ok)); inversion Abs. rewrite <- L in P_ok; generalize P_ok. simpl; set (k := map (apply_subst sigma) k1); clearbody k; set (p := P f); clearbody p. revert p k; fix projection_is_subterm 1. intro p; case p; clear p. intro l; case l; clear l. intro Abs; inversion Abs. intros t l _; simpl; left; reflexivity. intros p l; case l; clear l. intro Abs; inversion Abs. intros t l LL; simpl; right; generalize (projection_is_subterm p l (proj2 (Nat.succ_lt_mono _ _) LL)). case (nth_error l p). intros s s_in_l; exact s_in_l. intros Abs; apply False_rect; apply (Nat.lt_irrefl (size (Term f l))). apply size_direct_subterm; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)