proposition: Lemma interp_unicity : forall t, Interp_dom R1 R2 t -> forall s1 s2, Interp t s1 -> Interp t s2 -> s1 = s2.
proof: Proof. intros t Ht; assert (Acc_t :=interp_well_defined R1 R2 t Ht). induction Acc_t as [t Acc_t IH]. destruct t as [x | f l]; intros s1 S2 H1 H2; inversion H1 as [ | f1 l1 l1' ll1 Cf1 Hl1 Hl1' Hll1 | f1 l1 l1' ll1 Df1 Hl1 Hl1' Hll1 ]; inversion H2 as [ | f2 l2 l2' ll2 Cf2 Hl2 Hl2' Hll2 | f2 l2 l2' ll2 Df2 Hl2 Hl2' Hll2 ]; subst; trivial. apply (f_equal (fun ll => Term f (map (fun st => snd (A := term) st) ll))). assert (H : forall s s1 s2, In (s,s1) ll1 -> In (s,s2) ll2 -> s1 = s2). intros s s1 s2 ss1_in_ll1 ss2_in_ll2. assert (s_in_l : In s (map (fun st => fst st) ll1)). rewrite in_map_iff; exists (s,s1); split; trivial. apply IH with s; trivial. apply (Constr R1 R2 f (map (fun st => fst st) ll1) s Cf1 s_in_l). apply (interp_well_defined_1 R1 R2 _ _ Ht _ s_in_l). apply Hll1; trivial. apply Hll2; trivial. generalize ll1 ll2 Hl2 H; clear ll1 ll2 Hl2 H Hll1 Hll2 Ht Acc_t IH H2 H1. intro ll1; induction ll1 as [ | [s s1] ll1]; intros [ | [s' s2] ll2] H' H; trivial. discriminate. discriminate. simpl in H'; injection H'; clear H'; intros H' s_eq_s'; subst s'. rewrite (H s s1 s2); try (left; trivial). rewrite IHll1 with ll2; trivial. intros t t1 t2 tt1_in_ll1 tt2_in_ll2; apply (H t t1 t2); right; trivial. absurd (defined R2 f); trivial. absurd (defined R2 f); trivial. apply (f_equal (fun ll => Comb (map (fun st => snd (A := term) st) ll))). assert (H : forall s s1 s2, In (s,s1) ll1 -> In (s,s2) ll2 -> s1 = s2). intros s s1 s2 ss1_in_ll1 ss2_in_ll2. assert (s_in_l : In s (map (fun st => fst st) ll1)). rewrite in_map_iff; exists (s,s1); split; trivial. apply IH with s; trivial. apply (Defd R1 R2 f l s Df1). rewrite <- Hl1 in s_in_l. rewrite FB12; trivial. apply (interp_well_defined_2 R1 R2 f l Ht Df1 s). rewrite <- Hl1 in s_in_l. rewrite FB12; trivial. apply Hll1; trivial. apply Hll2; trivial. rewrite Hl1 in Hl2; generalize ll1 ll2 Hl2 H; clear ll1 ll2 Hl2 H Hll1 Hll2 Ht Acc_t IH H2 H1 Hl1. intro ll1; induction ll1 as [ | [s s1] ll1]; intros [ | [s' s2] ll2] H' H; trivial. discriminate. discriminate. simpl in H'; injection H'; clear H'; intros H' s_eq_s'; subst s'. rewrite (H s s1 s2); try (left; trivial). rewrite IHll1 with ll2; trivial. intros t t1 t2 tt1_in_ll1 tt2_in_ll2; apply (H t t1 t2); right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)