proposition: Lemma pow1_inv_eq: forall {T} (c:T) x y, pow1 c x = pow1 c y -> x = y.
proof: Proof. induction x; intros. - destruct y. { reflexivity. } inversion H. - simpl in *. destruct y. { inversion H. } inversion H; subst; clear H. apply IHx in H1. subst. reflexivity. Qed.
imports: Coq.Arith.Plus Coq.Arith.PeanoNat Coq.Lists.List