proposition: Lemma add_right_alias_O : forall (m : nat), add_right_alias O m = m.
proof: Proof. intros. autoinduct on add_right_alias || (idtac "step1 test8 fails (aliased constant)"; induction m). all: (simpl; congruence). Qed.
imports: Autoinduct(Autoinduct)