Inductive bool : Type :=
| true
| false.
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
Example test_orb1: (orb true false) = true.
Proof.
simpl. (* ===> true = true *)
reflexivity. (* ===> no more subgoals *)
Qed.β΄
Require Import Michocoq.macros. Import syntax.
Require Import Michocoq.semantics. Require Import Michocoq.util.
Import error.