proposition: Lemma eq_nat_dec_neq: forall (A: Type) n n' (s1 s2: A), (not (n = n')) -> (if eq_nat_dec n n' then s1 else s2) = s2.
proof: Proof. intros. destruct (eq_nat_dec n n'). exfalso. apply H in e. assumption. reflexivity. Qed.
imports: Coq(Bool Arith Arith.Peano_dec Arith.Compare_dec List)