Section Basics. Inductive maybe (A : Type) : Type := | defined : A -> maybe A | undefined : maybe A. Check maybe. Print maybe. Check maybe_ind. Variables A B : Type. Definition maybe_apply (f : A -> B) (ma : maybe A) : maybe B := match ma with | defined a => defined _ (f a) | undefined => undefined B end. Print bool. Definition is_defined (ma : maybe A) : bool := match ma with | defined _ => true | undefined => false end. Lemma bool_elim : forall (b : bool), b = true \/ b = false. Proof. intro b. destruct b as [ | ]. left. reflexivity. right. reflexivity. Qed. Print bool_elim. Lemma true_neq_false : ~ false = true. Proof. discriminate. Qed. Lemma is_defined_exists_defined : forall (ma : maybe A), is_defined ma = true -> exists (a : A), ma = defined A a. Proof. intros ma E. destruct ma as [a | ]. exists a. reflexivity. simpl in E. apply true_neq_false in E. destruct E. Qed. Lemma equal_defined_is_defined : forall (ma : maybe A) a, ma = defined _ a -> is_defined ma = true. Proof. intros ma a E. rewrite E. simpl. reflexivity. Qed. End Basics. Check maybe_apply.