proposition: Lemma atom_reduction : forall e t u, red t u -> is_atom e t -> is_atom e u.
proof: Proof. simple induction 1; intros; trivial. generalize (H1 H3); clear H1 H3. intros (n, lt_n, (l, eq_atom)). rewrite eq_atom in H2. split with n; trivial. generalize N H2; clear N H2 eq_atom H0. elim l; simpl in |- *; intros. inversion H2. inversion H2. apply False_ind. generalize H3. case l0; simpl in |- *; try intros tt ll; discriminate. elim H0 with (1 := H5); intros. rewrite H6. split with (a :: x); reflexivity. split with (N2 :: l0); reflexivity. Qed.
imports: Termes Types Conv Conv_Dec Strong_Norm Lia