proposition: Theorem andb_eq_orb : forall (b c : bool), (andb b c = orb b c) -> b = c.
proof: Proof. Admitted. Theorem add_assoc : forall n m p : nat, n + (m + p) = (n + m) + p. Proof. Admitted. Fixpoint nonzeros (lst : list nat) := match lst with | [] => [] | 0 :: t => nonzeros t | h :: t => h :: nonzeros t end. Lemma nonzeros_app : forall lst1 lst2 : list nat, nonzeros (lst1 ++ lst2) = (nonzeros lst1) ++ (nonzeros lst2). Proof. Admitted. Lemma re_opt_e_match' : forall T (re: reg_exp T) s, s =~ re -> s =~ re_opt_e re. Proof. intros T re s M. induction M as [| x' | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2 | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2]; simpl. - apply MEmpty. - apply MChar. - destruct re1; try (apply MApp; try apply IH1; apply IH2). inversion Hmatch1. simpl. apply IH2. - apply MUnionL. apply IH. - apply MUnionR. apply IH. - apply MStar0. - apply MStarApp. apply IH1. apply IH2. Qed.
imports: Coq(Arith List) LF(IndProp)