fact: Fixpoint interp_form (f:form): Prop := match f with [n]=> match get n env with PNone => True | PSome P => P end | A =>> B => (interp_form A) -> (interp_form B) | # => False | A //\\ B => (interp_form A) /\ (interp_form B) | A \\// B => (interp_form A) \/ (interp_form B) end.
imports: List Bintree Bool BinPos