(* (c) Copyright Christian Doczkal, Saarland University                   *)
(* Distributed under the terms of the CeCILL-B license                    *)

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrbool.

Ltac done := trivial; hnf in |- *; intros;
(
  solve [
    (do !
      [ solve [ trivial | apply : sym_equal; trivial ]
      | discriminate
      | contradiction
      | split
      | apply/andP;split
      | rewrite ?andbT ?andbF ?orbT ?orbF ]
    )
    | case not_locked_false_eq_true; assumption
    | match goal with
        | H:~ _ |- _ => solve [ case H; trivial ]
      end
  ]
).

(* TODO: what is going wring here?? 
Goal forall a b : bool, a && b.
move => ? ?.
(do !  solve [ trivial ] | match goal with  this may be useful, but also costly *)
| |- is_true (_ && _) => apply/andP;split end ).

match goal with  
| |- is_true (_ && _) => apply/andP;split
end.
*)