proposition: Lemma technical_lemma_1 : forall S1, @inclusion _ S1 R1 -> forall s s' t t', Interp_dom R1 R2 s -> Interp_dom R1 R2 t -> Interp s s' -> Interp t t' -> axiom (ddp S1) t s -> axiom (ddp S1) t' s'.
proof: Proof. intros S1 S1_in_R1 _s s' _t t' Is It Hs' Ht' t_S1_s. inversion t_S1_s as [t s sigma K]; clear t_S1_s; subst. destruct K as [K Sub]. inversion K as [ s'' t'' p f l t''_S1_s'' H Df H1 H2]; clear K; subst. destruct s as [v'' | f'' l'']. absurd (R1 t'' (Var v'')). apply R1_var. apply S1_in_R1; trivial. assert (H' := R1_at_top_dp _ S1_in_R1 _ _ _ _ t''_S1_s'' H sigma). destruct (H' Is) as [sigma' [Isigma [_ [Hs Ht]]]]; clear H'. rewrite (interp_unicity _ Is _ _ Hs' Hs). rewrite (interp_unicity _ It _ _ Ht' Ht). apply instance. split; [apply (Dp _ _ _ _ _ _ t''_S1_s'' H Df) | assumption]. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)