(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/decidable/".
-
(* classical connectives for decidable properties *)
include "decidable_kit/streicher.ma".
lemma prove_reflect : ∀P:Prop.∀b:bool.
(b = true → P) → (b = false → ¬P) → reflect P b.
-intros 2 (P b); cases b; intros; [left|right] autobatch.
+intros 2 (P b); cases b; intros; [left|right] [autobatch.|autobatch;]
qed.
(* ### standard connectives/relations with reflection predicate ### *)
lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
intros (n m); apply bool_to_eq; split; intros (H);
-[1:cases (b2pT ? ? (orbP ? ?) H); [2: autobatch]
+[1:cases (b2pT ? ? (orbP ? ?) H); [2: (*autobatch type;*) apply lebW; assumption; ]
rewrite > (eqb_true_to_eq ? ? H1); autobatch
|2:cases (b2pT ? ? (lebP ? ?) H);
[ elim n; [reflexivity|assumption]