proposition: Lemma negb_involutive' (n:nat) : forall b b2:bool, negb (negb b) = b.
proof: Proof. MProof. cintros b {- T.destruct b -};; T.select bool >>= T.clear ;; intros b2. - T.reflexivity. - T.reflexivity. Qed.
imports: Mtac2.Mtac2