proposition: Lemma one_step_unit_th_unit_nf_eq : forall t1 t2, one_step (sym_refl unit_one_step_at_top) t1 t2 -> unit_nf t1 = unit_nf t2.
proof: Proof. intro t1; pattern t1; apply term_rec3; clear t1. intros v t2 H; inversion H as [ t1 t2' H' | ]; subst; inversion H' as [[v1 | f1 l1] u2 sigma H'' v1_sigma u2_sigma]; destruct H'' as [ H'' | [H'' | H'']]. inversion H''. inversion H'' as [ u22 f u Ufu | u21 f u Ufu]. subst; simpl; rewrite v1_sigma; destruct Ufu as [Ufu | Ufu]; rewrite Ufu. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. subst; simpl; rewrite v1_sigma; destruct Ufu as [Ufu | Ufu]; rewrite Ufu. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. simpl. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. subst; trivial. intros f l IHl t2 H; inversion H as [t1 t2' H' | t1 t2' l2 H']; subst. generalize (no_need_of_instance _ _ H'); clear H'; intro H'. destruct H' as [H' | [H' | H']]. inversion H' as [t2' f' u [Ufu | Ufu] | t2' f' u [Ufu | Ufu]]; subst; simpl; rewrite Ufu. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. generalize (T.eq_bool_ok (unit_nf t2) (Term u nil)); case (T.eq_bool (unit_nf t2) (Term u nil)); [intro t2_eq_u | intro t2_diff_u]. apply sym_eq; trivial. trivial. generalize (Term f l) H'; clear H'; intros t H'; inversion H' as [t2' f' u [Ufu | Ufu] | t2' f' u [Ufu | Ufu]]; subst; simpl; rewrite Ufu. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. generalize (F.Symb.eq_bool_ok u u); case (F.Symb.eq_bool u u); [intros _; trivial | intro u_diff_u; apply False_rect; apply u_diff_u; reflexivity]. generalize (T.eq_bool_ok (unit_nf t) (Term u nil)); case (T.eq_bool (unit_nf t) (Term u nil)); [intro t_eq_u | intro t_diff_u]. trivial. trivial. subst; trivial. simpl; clear H; assert (map unit_nf l = map unit_nf l2). generalize l2 H'; clear l2 H'; induction l as [ | t l ]; intros l2 H; inversion H as [ t' t2 l' H' | t' l' l2' H']; subst; simpl. rewrite (IHl t (or_introl _ (eq_refl t)) t2 H'); trivial. apply (f_equal (fun l => unit_nf t :: l)); refine (IHl0 _ l2' H'); intros; apply IHl; trivial; right; trivial. clear IHl H'; destruct l as [ | t1 [ | t2 [ | t3 l]]]; destruct l2 as [ | s1 [ | s2 [ | s3 l2]]]; simpl in H; try discriminate. trivial. simpl; rewrite H; trivial. injection H; intros H1 H2; simpl; rewrite H1; rewrite H2; trivial. simpl; rewrite H; trivial. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)