proposition: Lemma Psi_unique : forall t s s', Psi s t -> Psi s' t -> s = s'.
proof: Proof. intros t; pattern t; apply term_rec3; clear t. intros v s s' P P'. assert False; [idtac | contradiction]. apply (Psi_not_nf (Var v) s); trivial. apply nf_var. intros f l IHl s s' P P'. inversion P as [ss tt H K | g ll H K]; inversion P' as [ss' tt' H' K' | g' ll' H' K']; clear P P'; subst. apply (UIR (Term f l)); trivial. unfold inner in K; simpl in K. destruct K' as [s' [t' [st_in_ll' P]]]. absurd (nf (one_step R) t'); trivial. apply K; rewrite in_map_iff; exists (s',t'); split; trivial. unfold inner in K'; simpl in K'. destruct K as [s [t [st_in_ll' P]]]. absurd (nf (one_step R) t); trivial. apply K'; rewrite in_map_iff; exists (s,t); split; trivial. apply (f_equal (fun l => Term f l)). generalize H ll' H' IHl H5; clear K K' H ll' H' IHl H5; induction ll as [ | [s t] ll]. intros _ [ | [s' t'] ll']; trivial; intros; discriminate. intros H1 [ | [s' t'] ll']; simpl; intros H' IHl H6. discriminate. injection H6; clear H6; intros H6 H7; subst t'. destruct (H1 s t (or_introl _ (eq_refl _))) as [P | [E I]]; destruct (H' s' t (or_introl _ (eq_refl _))) as [P' | [E' I']]. rewrite (IHl t (or_introl _ (eq_refl _)) s s'); trivial. apply (f_equal (fun l => s' :: l)). apply IHll; trivial. intros; apply H1; right; trivial. intros; apply H'; right; trivial. intros u u_in_ll v v'; apply IHl; right; trivial. subst s'; assert False; [idtac | contradiction]. apply (Psi_not_nf _ _ P I'). subst s; assert False; [idtac | contradiction]. apply (Psi_not_nf _ _ P' I). subst s s'; apply (f_equal (fun l => t :: l)). apply IHll; trivial. intros; apply H1; right; trivial. intros; apply H'; right; trivial. intros u u_in_ll v v'; apply IHl; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)