proposition: Lemma IsNull_cons : forall (a : bool) (v : BV), IsNull (consbv a v) = true -> IsNull v = true.
proof: Proof. simple induction a. simpl in |- *. intros. absurd (false = true). auto. exact H. intros v. auto. Qed.
imports: IncrDecr Memo