proposition: Lemma None_neq_Some : forall (AnyT AnyT' : Type) (a : AnyT), None = Some a -> AnyT'.
proof: Proof. intros; discriminate. Qed.
imports: Coq.Lists.List Coq.Strings.String Coq.Arith.Arith Coq.Logic.Eqdep_dec Fiat.Common.ilist Fiat.Common.ilist2