proposition: Lemma IsNull_BV_null : forall v : BV, IsNull v = true -> v = BV_null (lengthbv v).
proof: Proof. simple induction v. simpl in |- *. unfold BV_null in |- *. auto. intros a l H. intro. change (a :: l = false :: BV_null (lengthbv l)) in |- *. rewrite <- H. generalize H0. replace a with false. trivial. symmetry in |- *. apply IsNull_false with (v := l). exact H0. apply IsNull_cons with (a := a). exact H0. Qed.
imports: IncrDecr Memo