(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/decidable_kit/fgraph/".
-
include "decidable_kit/fintype.ma".
definition setA : ∀T:eqType.T → bool := λT,x.true.
[1: generalize in match H; rewrite > (b2pT ? ? (eqP (list_eqType d2) ? ?) H2);
intros; clear H H2; rewrite < (pirrel ? ? ? H1 H3 (eqType_decidable nat_eqType));
reflexivity
- |2: unfold Not; intros (H3); destruct H3; rewrite > Hcut in H2;
+ |2: unfold Not; intros (H3); destruct H3;
rewrite > (cmp_refl (list_eqType d2)) in H2; destruct H2;]
qed.
lemma mem_concat:
∀d:eqType. ∀x.∀l1,l2:list d.
mem d x (l1 @ l2) = orb (mem d x l1) (mem d x l2).
-intros; elim l1; [reflexivity] simplify; cases (cmp d x t); simplify; [reflexivity|assumption]
+intros; elim l1; [reflexivity] simplify; cases (cmp d x a); simplify; [reflexivity|assumption]
qed.
lemma orb_refl : ∀x.orb x x = x. intros (x); cases x; reflexivity; qed.
match x in list with [ nil ⇒ false | (cons he tl) ⇒ andb (mem ? he s) (mem ? tl l)].
intros (d s l x); elim s; [cases x] simplify; try reflexivity; rewrite > mem_concat;
rewrite > H; clear H; rewrite > mem_multes; cases x; simplify; [reflexivity]
-unfold list_eqType; simplify; apply (cmpP ? t s1); intros (E);
+unfold list_eqType; simplify; apply (cmpP ? a s1); intros (E);
cases (mem d s1 l1);
[1,2: rewrite > E; rewrite > cmp_refl; simplify;
[rewrite > orb_refl | rewrite > orbC ] reflexivity