helm/software/matita/nlibrary/datatypes/list.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/pts.ma".
  16 include "arithmetics/nat.ma".
  17
  18 ninductive list (A:Type[0]) : Type[0] ≝
  19   | nil: list A
  20   | cons: A -> list A -> list A.
  21
  22 notation "hvbox(hd break :: tl)"
  23   right associative with precedence 47
  24   for @{'cons $hd $tl}.
  25
  26 notation "[ list0 x sep ; ]"
  27   non associative with precedence 90
  28   for ${fold right @'nil rec acc @{'cons $x $acc}}.
  29
  30 notation "hvbox(l1 break @ l2)"
  31   right associative with precedence 47
  32   for @{'append $l1 $l2 }.
  33
  34 interpretation "nil" 'nil = (nil ?).
  35 interpretation "cons" 'cons hd tl = (cons ? hd tl).
  36
  37 nlet rec append A (l1: list A) l2 on l1 ≝
  38   match l1 with
  39   [ nil ⇒ l2
  40   | cons hd tl ⇒ hd :: append A tl l2 ].
  41
  42 interpretation "append" 'append l1 l2 = (append ? l1 l2).
  43
  44 nlet rec id_list A (l: list A) on l ≝
  45   match l with
  46   [ nil ⇒ []
  47   | cons hd tl ⇒ hd :: id_list A tl ].
  48
  49
  50 ndefinition tail ≝ λA:Type[0].λl:list A.
  51   match l with
  52   [ nil ⇒  []
  53   | cons hd tl ⇒  tl].
  54
  55 nlet rec flatten S (l : list (list S)) on l : list S ≝
  56 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
  57
  58 ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
  59 #A;#l;nelim l;//;
  60 #a;#l1;#IH;nnormalize;
  61 nrewrite > IH;//;
  62 nqed.
  63
  64 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
  65 #A;#x;#y;#z;nelim x
  66 ##[//
  67 ##|#a;#x1;#H;nnormalize;//]
  68 nqed.
  69
  70 ntheorem cons_append_commute:
  71   ∀A:Type[0].∀l1,l2:list A.∀a:A.
  72     a :: (l1 @ l2) = (a :: l1) @ l2.
  73 //;
  74 nqed.
  75
  76 nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
  77 #A;#a;#l;#l1;nrewrite > (associative_append ????);//;
  78 nqed.
  79
  80 (*ninductive permutation (A:Type) : list A -> list A -> Prop \def
  81   | refl : \forall l:list A. permutation ? l l
  82   | swap : \forall l:list A. \forall x,y:A.
  83               permutation ? (x :: y :: l) (y :: x :: l)
  84   | trans : \forall l1,l2,l3:list A.
  85               permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3
  86 with permut1 : list A -> list A -> Prop \def
  87   | step : \forall l1,l2:list A. \forall x,y:A.
  88       permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*)
  89
  90 (*
  91
  92 definition x1 \def S O.
  93 definition x2 \def S x1.
  94 definition x3 \def S x2.
  95
  96 theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []).
  97   apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?).
  98   apply refl.
  99   apply (step ? (x1::[]) [] x2 x3).
 100   qed.
 101
 102 theorem nil_append_nil_both:
 103   \forall A:Type.\forall l1,l2:list A.
 104     l1 @ l2 = [] \to l1 = [] \land l2 = [].
 105
 106 theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: [].
 107 reflexivity.
 108 qed.
 109
 110 theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O].
 111 simplify.
 112 reflexivity.
 113 qed.
 114
 115 *)
 116
 117 nlet rec nth A l d n on l ≝
 118   match l with
 119   [ nil ⇒ d
 120   | cons (x:A) tl ⇒ match n with
 121     [ O ⇒ x
 122     | S n' ⇒ nth A tl d n' ] ].
 123
 124 nlet rec map A B f l on l ≝
 125   match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ].
 126
 127 nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝
 128   match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
 129
 130 ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
 131
 132 ndefinition filter ≝
 133   λT:Type[0].λl:list T.λp:T → bool.
 134   foldr T (list T)
 135     (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
 136
 137 ndefinition iota : nat → nat → list nat ≝
 138   λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
 139
 140 (* ### induction principle for functions visiting 2 lists in parallel *)
 141 nlemma list_ind2 :
 142   ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
 143   length ? l1 = length ? l2 →
 144   (P (nil ?) (nil ?)) →
 145   (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
 146   P l1 l2.
 147 #T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons;
 148 ngeneralize in match Hl; ngeneralize in match l2;
 149 nelim l1
 150 ##[#l2;ncases l2;//;
 151    nnormalize;#t2;#tl2;#H;ndestruct;
 152 ##|#t1;#tl1;#IH;#l2;ncases l2
 153    ##[nnormalize;#H;ndestruct
 154    ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//]
 155 ##]
 156 nqed.
 157
 158 nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 159 #A;#B;#f;#g;#l;#Efg;
 160 nelim l; nnormalize;//;
 161 nqed.
 162
 163 nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l.
 164 #A;#l;#p;nelim l;nnormalize
 165 ##[//
 166 ##|#a;#tl;#IH;ncases (p a);nnormalize;
 167    ##[napply le_S_S;//;
 168    ##|@2;//]
 169 ##]
 170 nqed.
 171
 172 nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m.
 173 #A;#l;#m;nelim l;
 174 ##[//
 175 ##|#H;#tl;#IH;nnormalize;nrewrite < IH;//]
 176 nqed.
 177
 178 ninductive in_list (A:Type): A → (list A) → Prop ≝
 179 | in_list_head : ∀ x,l.(in_list A x (x::l))
 180 | in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)).
 181
 182 ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def
 183   \lambda A,l,m.\forall x.in_list A x l \to in_list A x m.
 184
 185 notation "hvbox(a break ∉ b)" non associative with precedence 45
 186 for @{ 'notmem $a $b }.
 187
 188 interpretation "list member" 'mem x l = (in_list ? x l).
 189 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
 190 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
 191
 192 nlemma not_in_list_nil : \forall A,x.\lnot in_list A x [].
 193 #A x;@;#H1;ninversion H1;
 194 ##[#a0 al0 H2 H3;ndestruct (H3);
 195 ##|#a0 a1 al0 H2 H3 H4 H5;ndestruct (H5)
 196 ##]
 197 nqed.
 198
 199 nlemma in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to
 200                           x = a \lor in_list A x l.
 201 #A a0 a1 al0 H1;ninversion H1
 202 ##[#a2 al1 H2 H3;ndestruct (H3);@;@
 203 ##|#a2 a3 al1 H2 H3 H4 H5;ndestruct (H5);@2;//
 204 ##]
 205 nqed.
 206
 207 nlemma in_list_tail : \forall A,l,x,y.
 208       in_list A x (y::l) \to x \neq y \to in_list A x l.
 209 #A;#l;#x;#y;#H;#Hneq;
 210 ninversion H;
 211 ##[#x1;#l1;#Hx;#Hl;ndestruct;nelim Hneq;#Hfalse;
 212    nelim (Hfalse ?);@;
 213 ##|#x1;#y1;#l1;#H1;#_;#Hx;#Heq;ndestruct;//;
 214 ##]
 215 nqed.
 216
 217 nlemma in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y.
 218 #A a0 a1 H1;ncases (in_list_cons_case ???? H1)
 219 ##[//
 220 ##|#H2;napply False_ind;ncases (not_in_list_nil ? a0);#H3;/2/
 221 ##]
 222 nqed.
 223
 224 nlemma in_list_to_in_list_append_l: \forall A.\forall x:A.
 225 \forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2).
 226 #A a0 al0 al1 H1;nelim H1
 227 ##[#a1 al2;@;
 228 ##|#a1 a2 al2 H2 H3;@2;//
 229 ##]
 230 nqed.
 231
 232 nlemma in_list_to_in_list_append_r: \forall A.\forall x:A.
 233 \forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2).
 234 #A a0 al0 al1 H1;nelim al0
 235 ##[napply H1
 236 ##|#a1 al2 IH;@2;napply IH
 237 ##]
 238 nqed.
 239
 240 nlemma in_list_append_to_or_in_list: \forall A:Type.\forall x:A.
 241 \forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1.
 242 #A a0 al0;nelim al0
 243 ##[#al1 H1;@2;napply H1
 244 ##|#a1 al1 IH al2 H1;nnormalize in H1;
 245    ncases (in_list_cons_case ???? H1);#H2
 246    ##[@;nrewrite > H2;@
 247    ##|ncases (IH … H2);#H3
 248       ##[@;@2;//
 249       ##|@2;//
 250       ##]
 251    ##]
 252 ##]
 253 nqed.
 254
 255 nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
 256  match l with
 257   [ nil ⇒ false
 258   | (cons a l') ⇒
 259     match eq x a with
 260      [ true ⇒ true
 261      | false ⇒ mem A eq x l'
 262      ]
 263   ].
 264
 265 nlemma mem_true_to_in_list :
 266   \forall A,equ.
 267   (\forall x,y.equ x y = true \to x = y) \to
 268   \forall x,l.mem A equ x l = true \to in_list A x l.
 269 #A equ H1 a0 al0;nelim al0
 270 ##[nnormalize;#H2;ndestruct (H2)
 271 ##|#a1 al1 IH H2;nwhd in H2:(??%?);
 272    nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3
 273    ##[nrewrite > (H1 … H3);@
 274    ##|@2;napply IH;nrewrite > H3 in H2;nnormalize;//;
 275    ##]
 276 ##]
 277 nqed.
 278
 279 nlemma in_list_to_mem_true :
 280   \forall A,equ.
 281   (\forall x.equ x x = true) \to
 282   \forall x,l.in_list A x l \to mem A equ x l = true.
 283 #A equ H1 a0 al0;nelim al0
 284 ##[#H2;napply False_ind;ncases (not_in_list_nil ? a0);/2/
 285 ##|#a1 al1 IH H2;nelim H2
 286    ##[nnormalize;#a2 al2;nrewrite > (H1 …);@
 287    ##|#a2 a3 al2 H3 H4;nnormalize;ncases (equ a2 a3);nnormalize;//;
 288    ##]
 289 ##]
 290 nqed.
 291
 292 nlemma in_list_filter_to_p_true : \forall A,l,x,p.
 293 in_list A x (filter A l p) \to p x = true.
 294 #A al0 a0 p;nelim al0
 295 ##[nnormalize;#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
 296 ##|#a1 al1 IH H1;nnormalize in H1;nlapply (refl ? (p a1));
 297    ngeneralize in match H1;ncases (p a1) in ⊢ (???% -> ???% → %);
 298    ##[#H2 H3;ncases (in_list_cons_case ???? H2);#H4
 299       ##[nrewrite > H4;//
 300       ##|napply (IH H4);
 301       ##]
 302    ##|#H2 H3;napply (IH H2);
 303    ##]
 304 ##]
 305 nqed.
 306
 307 nlemma in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
 308 #A al0 p a0;nelim al0
 309 ##[nnormalize;//;
 310 ##|#a1 al1 IH H1;nnormalize in H1;
 311    nlapply (refl ? (p a1));ncases (p a1) in ⊢ (???% → %);#H2
 312    ##[nrewrite > H2 in H1;#H1;ncases (in_list_cons_case ???? H1);#H3
 313       ##[nrewrite > H3;@
 314       ##|@2;napply IH;napply H3
 315       ##]
 316    ##|@2;napply IH;nrewrite > H2 in H1;#H1;napply H1;
 317    ##]
 318 ##]
 319 nqed.
 320
 321 nlemma in_list_filter_r : \forall A,l,p,x.
 322               in_list A x l \to p x = true \to in_list A x (filter A l p).
 323 #A al0 p a0;nelim al0
 324 ##[#H1;napply False_ind;ncases (not_in_list_nil ? a0);/2/
 325 ##|#a1 al1 IH H1 H2;ncases (in_list_cons_case ???? H1);#H3
 326    ##[nnormalize;nrewrite < H3;nrewrite > H2;@
 327    ##|nnormalize;ncases (p a1);nnormalize;
 328       ##[@2;napply IH;//
 329       ##|napply IH;//
 330       ##]
 331    ##]
 332 ##]
 333 nqed.
 334
 335 nlemma incl_A_A: ∀T,A.incl T A A.
 336 #A al0 a0 H1;//;
 337 nqed.
 338
 339 nlemma incl_append_l : ∀T,A,B.incl T A (A @ B).
 340 #A al0 al1 a0 H1;/2/;
 341 nqed.
 342
 343 nlemma incl_append_r : ∀T,A,B.incl T B (A @ B).
 344 #A al0 al1 a0 H1;/2/;
 345 nqed.
 346
 347 nlemma incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
 348 #A al0 al1 a0 H1 a1 H2;ncases (in_list_cons_case ???? H2);/2/;
 349 #H3;@2;napply H1;//;
 350 nqed.
 351
 352 nlet rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l ≝
 353  match l with
 354  [ nil ⇒ a
 355  | cons b bl ⇒ foldl A B f (f a b) bl ].
 356
 357 nlet rec foldl2 (A,B,C:Type[0]) (f:A → B → C → A) (a:A) (bl:list B) (cl:list C) on bl ≝
 358  match bl with
 359  [ nil ⇒ a
 360  | cons b0 bl0 ⇒ match cl with
 361    [ nil ⇒ a
 362    | cons c0 cl0 ⇒ foldl2 A B C f (f a b0 c0) bl0 cl0 ] ].
 363
 364 nlet rec foldr2 (A,B : Type[0]) (X : Type[0]) (f: A → B → X → X) (x:X)
 365                 (al : list A) (bl : list B) on al : X ≝
 366   match al with
 367   [ nil ⇒ x
 368   | cons a al1 ⇒ match bl with
 369     [ nil ⇒ x
 370     | cons b bl1 ⇒ f a b (foldr2 ??? f x al1 bl1) ] ].
 371
 372 nlet rec rev (A:Type[0]) (l:list A) on l ≝
 373  match l with
 374  [ nil ⇒ nil A
 375  | cons hd tl ⇒ (rev A tl)@[hd] ].
 376
 377 notation > "hvbox(a break \liff b)"
 378   left associative with precedence 25
 379 for @{ 'iff $a $b }.
 380
 381 notation "hvbox(a break \leftrightarrow b)"
 382   left associative with precedence 25
 383 for @{ 'iff $a $b }.
 384
 385 interpretation "logical iff" 'iff x y = (iff x y).
 386
 387 ndefinition coincl : ∀A.list A → list A → Prop ≝  λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.
 388
 389 notation > "hvbox(a break ≡ b)"
 390   non associative with precedence 45
 391 for @{'equiv $a $b}.
 392
 393 notation < "hvbox(term 46 a break ≡ term 46 b)"
 394   non associative with precedence 45
 395 for @{'equiv $a $b}.
 396
 397 interpretation "list coinclusion" 'equiv x y = (coincl ? x y).
 398
 399 nlemma refl_coincl : ∀A.∀l:list A.l ≡ l.
 400 #;@;#;//;
 401 nqed.
 402
 403 nlemma coincl_rev : ∀A.∀l:list A.l ≡ rev ? l.
 404 #A l x;@;nelim l
 405 ##[##1,3:#H;napply False_ind;ncases (not_in_list_nil ? x);
 406    #H1;napply (H1 H);
 407 ##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
 408    ##[napply in_list_to_in_list_append_r;nrewrite > H1;@
 409    ##|napply in_list_to_in_list_append_l;/2/
 410    ##]
 411 ##|#a l0 IH H;ncases (in_list_append_to_or_in_list ???? H);#H1
 412    ##[/3/;
 413    ##|nrewrite > (in_list_singleton_to_eq ??? H1);@
 414    ##]
 415 ##]
 416 nqed.
 417
 418 nlemma not_in_list_nil_r : ∀A.∀l:list A.l = [] → ∀x.x ∉ l.
 419 #A l;nelim l
 420 ##[#;napply not_in_list_nil
 421 ##|#a l0 IH Hfalse;ndestruct (Hfalse)
 422 ##]
 423 nqed.
 424
 425 nlemma eq_filter_append :
 426  ∀A,p,l1,l2.filter A (l1@l2) p = filter A l1 p@filter A l2 p.
 427 #A p l1 l2;nelim l1
 428 ##[@
 429 ##|#a0 l0 IH;nwhd in ⊢ (??%(??%?));ncases (p a0)
 430    ##[nwhd in ⊢ (??%%);nrewrite < IH;@
 431    ##|nwhd in ⊢ (??%(??%?));nrewrite < IH;@
 432    ##]
 433 ##]
 434 nqed.
 435
 436 nlemma map_ind :
 437  ∀A,B:Type[0].∀f:A→B.∀P:B → Prop.
 438   ∀al.(∀a.a ∈ al → P (f a)) →
 439   ∀b. b ∈ map ?? f al → P b.
 440 #A B f P al;nelim al
 441 ##[#H1 b Hfalse;napply False_ind;
 442    ncases (not_in_list_nil ? b);#H2;napply H2;napply Hfalse;
 443 ##|#a1 al1 IH H1 b Hin;nwhd in Hin:(???%);ncases (in_list_cons_case ???? Hin);
 444    ##[#e;nrewrite > e;napply H1;@
 445    ##|#Hin1;napply IH;
 446       ##[#a2 Hin2;napply H1;@2;//;
 447       ##|//
 448       ##]
 449    ##]
 450 ##]
 451 nqed.
 452
 453 nlemma map_compose :
 454  ∀A,B,C,f,g,l.map B C f (map A B g l) = map A C (λx.f (g x)) l.
 455 #A B C f g l;nelim l
 456 ##[@
 457 ##|#a0 al0 IH;nchange in ⊢ (??%%) with (cons ???);
 458    napply eq_f2; //;
 459 ##]
 460 nqed.
 461
 462 nlemma incl_incl_to_incl_append :
 463   ∀A.∀l1,l2,l1',l2':list A.l1 ⊆ l1' → l2 ⊆ l2' → l1@l2 ⊆ l1'@l2'.
 464 #A al0 al1 al2 al3 H1 H2 a0 H3;
 465 ncases (in_list_append_to_or_in_list ???? H3);#H4;
 466 ##[napply in_list_to_in_list_append_l;napply H1;//
 467 ##|napply in_list_to_in_list_append_r;napply H2;//
 468 ##]
 469 nqed.
 470
 471 nlemma eq_map_append :
 472   ∀A,B,f,l1,l2.map A B f (l1@l2) = map A B f l1@map A B f l2.
 473 #A B f al1 al2;nelim al1
 474 ##[@
 475 ##|#a0 al3 IH;nnormalize;nrewrite > IH;@;
 476 ##]
 477 nqed.
 478
 479 nlemma not_in_list_to_mem_false :
 480   ∀A,equ.
 481   (∀x,y.equ x y = true → x = y) →
 482   ∀x:A.∀l. x ∉ l → mem A equ x l = false.
 483 #A equ H1 a0 al0;nelim al0
 484 ##[#_;@
 485 ##|#a1 al1 IH H2;nwhd in ⊢ (??%?);
 486    nlapply (refl ? (equ a0 a1));ncases (equ a0 a1) in ⊢ (???% → %);#H3;
 487    ##[napply False_ind;ncases H2;#H4;napply H4;
 488       nrewrite > (H1 … H3);@
 489    ##|napply IH;@;#H4;ncases H2;#H5;napply H5;@2;//
 490    ##]
 491 ##]
 492 nqed.
 493
 494 nlet rec list_forall (A:Type[0]) (l:list A) (p:A → bool) on l : bool ≝
 495  match l with
 496  [ nil ⇒ (true:bool)
 497  | cons a al ⇒ p a ∧ list_forall A al p ].
 498
 499 nlemma eq_map_f_g :
 500  ∀A,B,f,g,xl.(∀x.x ∈ xl → f x = g x) → map A B f xl = map A B g xl.
 501 #A B f g xl;nelim xl
 502 ##[#;@
 503 ##|#a al IH H1;nwhd in ⊢ (??%%);napply eq_f2
 504    ##[napply H1;@;
 505    ##|napply IH;#x Hx;napply H1;@2;//
 506    ##]
 507 ##]
 508 nqed.
 509
 510 nlemma x_in_map_to_eq :
 511   ∀A,B,f,x,l.x ∈ map A B f l → ∃x'.x = f x' ∧ x' ∈ l.
 512 #A B f x l;nelim l
 513 ##[#H;ncases (not_in_list_nil ? x);#H1;napply False_ind;napply (H1 H)
 514 ##|#a l0 IH H;ncases (in_list_cons_case ???? H);#H1
 515    ##[nrewrite > H1;@ a;@;@
 516    ##|ncases (IH H1);#a0;*;#H2 H3;@a0;@
 517       ##[// ##|@2;// ##]
 518    ##]
 519 ##]
 520 nqed.
 521
 522 nlemma list_forall_false :
 523  ∀A:Type[0].∀x,xl,p. p x = false → x ∈ xl → list_forall A xl p = false.
 524 #A x xl p H1;nelim xl
 525 ##[#Hfalse;napply False_ind;ncases (not_in_list_nil ? x);#H2;napply (H2 Hfalse)
 526 ##|#x0 xl0 IH H2;ncases (in_list_cons_case ???? H2);#H3
 527    ##[nwhd in ⊢ (??%?);nrewrite < H3;nrewrite > H1;@
 528    ##|nwhd in ⊢ (??%?);ncases (p x0)
 529       ##[nrewrite > (IH H3);@
 530       ##|@
 531       ##]
 532    ##]
 533 ##]
 534 nqed.
 535
 536 nlemma list_forall_true :
 537  ∀A:Type[0].∀xl,p. (∀x.x ∈ xl → p x = true) → list_forall A xl p = true.
 538 #A xl p;nelim xl
 539 ##[#;@
 540 ##|#x0 xl0 IH H1;nwhd in ⊢ (??%?);nrewrite > (H1 …)
 541    ##[napply IH;#x Hx;napply H1;@2;//
 542    ##|@
 543    ##]
 544 ##]
 545 nqed.