proposition: Lemma well_formed_unit_nf : forall t, well_formed t -> well_formed (unit_nf t).
proof: Proof. unfold well_formed; intro t; pattern t; apply term_rec3; clear t. intros v _; simpl; trivial. intros f l IHl Wt; generalize (well_formed_unfold Wt); clear Wt; intros [Wl Ar]; unfold well_formed in Wl. assert (Wl' : forall u, In u (map unit_nf l) -> well_formed_bool u = true). clear Ar; induction l as [ | t l]. contradiction. intros u [u_eq | In_u]. subst; apply IHl; [idtac | apply Wl]; left; trivial. apply IHl0; trivial; intros; [ apply IHl; trivial | apply Wl]; right; trivial. simpl; generalize (length_map unit_nf l); intro L; rewrite <- L in Ar; clear L. destruct l as [ | t1 [ | t2 [ | t3 l ]]]; simpl in Ar; simpl in Wl'. simpl; destruct (arity f) as [ | | [ | n]]; try (discriminate || trivial). simpl; destruct (arity f) as [ | | [ | n]]; try (discriminate || trivial). injection Ar; intro; subst; rewrite Wl'; [reflexivity | left; reflexivity]. destruct (unit_theory f) as [ u | u | u | ]. generalize (T.eq_bool_ok (unit_nf t1) (Term u nil)); case (T.eq_bool (unit_nf t1) (Term u nil)); [intro t1_eq_u | intro t1_diff_u]. apply Wl'; right; left; trivial. apply well_formed_fold; intuition. 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 Wl'; left; trivial. apply well_formed_fold; intuition. generalize (T.eq_bool_ok (unit_nf t1) (Term u nil)); case (T.eq_bool (unit_nf t1) (Term u nil)); [intro t1_eq_u | intro t1_diff_u]. apply Wl'; right; left; trivial. 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 Wl'; left; trivial. apply well_formed_fold; intuition. apply well_formed_fold; intuition. rewrite length_map in Ar; simpl. destruct (arity f) as [ | | n]; try discriminate. subst n; rewrite length_map. rewrite Nat.eqb_refl; rewrite Bool.andb_true_r. rewrite (IHl t1); simpl. rewrite (IHl t2); simpl. rewrite (IHl t3); simpl. assert (Wl'' : forall u : term, In u (map unit_nf l) -> well_formed u). intros; apply Wl'; right; right; right; trivial. clear t1 t2 t3 IHl Wl Wl'; revert l Wl''. intro l; induction l as [ | t l]; simpl. trivial. intro H; rewrite H. rewrite IHl; trivial. intros; apply H; right; trivial. left; trivial. do 2 right; left; trivial. apply Wl; do 2 right; left; trivial. right; left; trivial. apply Wl; right; left; trivial. left; trivial. apply Wl; left; trivial. Qed.
imports: Coq(Arith List Relations) CoLoR(closure more_list weaved_relation list_sort term_spec equational_theory ac cf_eq_ac rpo)