fact: Fixpoint L_value (l : L): bool := match l with | L_true => true | L_false => false | L_disj l1 l2 => L_value l1 || L_value l2 | L_conj l1 l2 => L_value l1 && L_value l2 | L_impl l1 l2 => implb (L_value l1) (L_value l2) | L_not l1 => negb (L_value l1) end.
imports: Bool