proposition: Lemma sub_projection : (forall u v, cdp v u -> connect_approx (u0,v0) (u,v) -> connect_approx (u,v) (u0,v0) -> refl_trans_clos (union _ (one_step R) direct_subterm) (projection v) (projection u)) -> forall t1 t2 t3, R1 t3 t2 -> R1 t2 t1 -> trans_clos (union term (one_step R) direct_subterm) (projection t2) (projection t1).
proof: Proof. intros Hdp t1 t3 t5 H53 H31. inversion H31 as [t3' t2 t1' H32 H21]; subst t1' t3'. inversion H53 as [t5' t4 t3' H54 H43]; subst t3' t5'. assert (B21 := dp0_decreases _ _ H21). assert (B32 := between_dp0 Hdp t1 t2 t3 t4 H21 H32 H43). inversion B32 as [t | t4' t3' B32']. rewrite H0; assumption. apply trans_clos_is_trans with (projection t2); assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)