proposition: Lemma re_opt_match' : forall T (re: reg_exp T) s, s =~ re -> s =~ re_opt re.
proof: Proof. Admitted. Definition manual_grade_for_re_opt : option (nat*string) := None. Theorem hyp_name : forall (P : Prop), P -> P. Proof. intros P HP. apply HP. Qed.
imports: Coq(Arith List) LF(IndProp)