proposition: Lemma eq_nat_dec_eq: forall (A: Type) n (s1 s2: A), (if eq_nat_dec n n then s1 else s2) = s1.
proof: Proof. intros. destruct (eq_nat_dec n n). reflexivity. exfalso. apply n0. reflexivity. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)