Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Paths Types.Unit Types.Prod.Require Export Spaces.List.Core.(** * Theory of Lists and List Operations *)(** In this file we collect lemmas about lists and their operations. We don't include those in [List.Core] so that file can stay lightweight on dependencies. *)(** We generally try to keep the order the same as the concepts appeared in [List.Core]. *)LocalOpen Scope list_scope.(** ** Concatenation *)(** Associativity of list concatenation. *)
A: Type x, y, z: list A
x ++ y ++ z = (x ++ y) ++ z
A: Type x, y, z: list A
x ++ y ++ z = (x ++ y) ++ z
A: Type y, z: list A
nil ++ y ++ z = (nil ++ y) ++ z
A: Type a: A x, y, z: list A IHx: x ++ y ++ z = (x ++ y) ++ z
(a :: x) ++ y ++ z = ((a :: x) ++ y) ++ z
A: Type y, z: list A
nil ++ y ++ z = (nil ++ y) ++ z
reflexivity.
A: Type a: A x, y, z: list A IHx: x ++ y ++ z = (x ++ y) ++ z
(a :: x) ++ y ++ z = ((a :: x) ++ y) ++ z
exact (ap (cons a) IHx).Defined.(** The type of lists has a monoidal structure given by concatenation. *)
A: Type w, x, y, z: list A
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z =
(ap (funl : list A => w ++ l) (app_assoc x y z) @
app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y)
A: Type w, x, y, z: list A
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z =
(ap (funl : list A => w ++ l) (app_assoc x y z) @
app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y)
A: Type w, x, y, z: list A
(ap (funl : list A => w ++ l) (app_assoc x y z) @
app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
A: Type x, y, z: list A
(ap (funl : list A => nil ++ l) (app_assoc x y z) @
app_assoc nil (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc nil x y) =
app_assoc nil x (y ++ z) @ app_assoc (nil ++ x) y z
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (funl : list A => (a :: w) ++ l)
(app_assoc x y z) @ app_assoc (a :: w) (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc (a :: w) x y) =
app_assoc (a :: w) x (y ++ z) @
app_assoc ((a :: w) ++ x) y z
A: Type x, y, z: list A
(ap (funl : list A => nil ++ l) (app_assoc x y z) @
app_assoc nil (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc nil x y) =
app_assoc nil x (y ++ z) @ app_assoc (nil ++ x) y z
A: Type x, y, z: list A
(ap idmap (app_assoc x y z) @ 1) @ 1 =
1 @ app_assoc x y z
A: Type x, y, z: list A
ap idmap (app_assoc x y z) @ 1 = app_assoc x y z
A: Type x, y, z: list A
ap idmap (app_assoc x y z) = app_assoc x y z
apply ap_idmap.
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (funl : list A => (a :: w) ++ l)
(app_assoc x y z) @ app_assoc (a :: w) (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc (a :: w) x y) =
app_assoc (a :: w) x (y ++ z) @
app_assoc ((a :: w) ++ x) y z
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (funl : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z)) @
ap (funl : list A => l ++ z)
(ap (cons a) (app_assoc w x y)) =
ap (cons a) (app_assoc w x (y ++ z)) @
ap (cons a) (app_assoc (w ++ x) y z)
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (funl : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z)) @
ap (funl : list A => l ++ z)
(ap (cons a) (app_assoc w x y)) =
ap (cons a)
(app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z)
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (funl : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z)) @
ap (funl : list A => l ++ z)
(ap (cons a) (app_assoc w x y)) =
ap (cons a)
((ap (funl : list A => w ++ l) (app_assoc x y z) @
app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y))
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
(ap (funl : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z)) @
ap (funl : list A => l ++ z)
(ap (cons a) (app_assoc w x y)) =
ap (cons a)
(ap (funl : list A => w ++ l) (app_assoc x y z) @
app_assoc w (x ++ y) z) @
ap (cons a)
(ap (funl : list A => l ++ z) (app_assoc w x y))
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (funl : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z) =
ap (cons a)
(ap (funl : list A => w ++ l) (app_assoc x y z) @
app_assoc w (x ++ y) z)
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (funl : list A => l ++ z)
(ap (cons a) (app_assoc w x y)) =
ap (cons a)
(ap (funl : list A => l ++ z) (app_assoc w x y))
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (funl : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z) =
ap (cons a)
(ap (funl : list A => w ++ l) (app_assoc x y z) @
app_assoc w (x ++ y) z)
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (funl : list A => a :: w ++ l) (app_assoc x y z) @
ap (cons a) (app_assoc w (x ++ y) z) =
ap (cons a)
(ap (funl : list A => w ++ l) (app_assoc x y z)) @
ap (cons a) (app_assoc w (x ++ y) z)
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (funl : list A => a :: w ++ l) (app_assoc x y z) =
ap (cons a)
(ap (funl : list A => w ++ l) (app_assoc x y z))
apply ap_compose.
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (funl : list A => l ++ z)
(ap (cons a) (app_assoc w x y)) =
ap (cons a)
(ap (funl : list A => l ++ z) (app_assoc w x y))
A: Type a: A w, x, y, z: list A IHw: forallxyz : list A,
(ap (funl : list A => w ++ l) (app_assoc x y z) @ app_assoc w (x ++ y) z) @
ap (funl : list A => l ++ z) (app_assoc w x y) =
app_assoc w x (y ++ z) @ app_assoc (w ++ x) y z
ap (funx : list A => (a :: x) ++ z) (app_assoc w x y) =
ap (cons a)
(ap (funl : list A => l ++ z) (app_assoc w x y))
nrapply (ap_compose (funl => l ++ z)).Defined.(** ** Folding *)
A, B: Type f: A -> B -> A l, l': list B i: A
fold_left f (l ++ l') i =
fold_left f l' (fold_left f l i)
A, B: Type f: A -> B -> A l, l': list B i: A
fold_left f (l ++ l') i =
fold_left f l' (fold_left f l i)
A, B: Type f: A -> B -> A l': list B i: A
fold_left f (nil ++ l') i =
fold_left f l' (fold_left f nil i)
A, B: Type f: A -> B -> A a: B l, l': list B i: A IHl: foralli : A, fold_left f (l ++ l') i = fold_left f l' (fold_left f l i)
fold_left f ((a :: l) ++ l') i =
fold_left f l' (fold_left f (a :: l) i)
A, B: Type f: A -> B -> A a: B l, l': list B i: A IHl: foralli : A, fold_left f (l ++ l') i = fold_left f l' (fold_left f l i)
fold_left f ((a :: l) ++ l') i =
fold_left f l' (fold_left f (a :: l) i)
apply IHl.Defined.
A, B: Type f: B -> A -> A i: A l, l': list B
fold_right f i (l ++ l') =
fold_right f (fold_right f i l') l
A, B: Type f: B -> A -> A i: A l, l': list B
fold_right f i (l ++ l') =
fold_right f (fold_right f i l') l
A, B: Type f: B -> A -> A i: A l': list B
fold_right f i (nil ++ l') =
fold_right f (fold_right f i l') nil
A, B: Type f: B -> A -> A i: A a: B l, l': list B IHl: foralli : A, fold_right f i (l ++ l') = fold_right f (fold_right f i l') l
fold_right f i ((a :: l) ++ l') =
fold_right f (fold_right f i l') (a :: l)
A, B: Type f: B -> A -> A i: A a: B l, l': list B IHl: foralli : A, fold_right f i (l ++ l') = fold_right f (fold_right f i l') l
fold_right f i ((a :: l) ++ l') =
fold_right f (fold_right f i l') (a :: l)
exact (ap (f a) (IHl _)).Defined.(** ** Maps *)
A: Type f: A -> A Hf: forallx : A, f x = x l: list A
map f l = l
A: Type f: A -> A Hf: forallx : A, f x = x l: list A
map f l = l
A: Type f: A -> A Hf: forallx : A, f x = x
map f nil = nil
A: Type f: A -> A Hf: forallx : A, f x = x x: A l: list A IHl: map f l = l
map f (x :: l) = x :: l
A: Type f: A -> A Hf: forallx : A, f x = x
map f nil = nil
reflexivity.
A: Type f: A -> A Hf: forallx : A, f x = x x: A l: list A IHl: map f l = l
map f (x :: l) = x :: l
A: Type f: A -> A Hf: forallx : A, f x = x x: A l: list A IHl: map f l = l
f x :: map f l = x :: l
A: Type f: A -> A Hf: forallx : A, f x = x x: A l: list A IHl: map f l = l
f x = x
A: Type f: A -> A Hf: forallx : A, f x = x x: A l: list A IHl: map f l = l
map f l = l
A: Type f: A -> A Hf: forallx : A, f x = x x: A l: list A IHl: map f l = l
f x = x
exact (Hf _).
A: Type f: A -> A Hf: forallx : A, f x = x x: A l: list A IHl: map f l = l
map f l = l
exact IHl.Defined.
A, B, C: Type f: A -> B -> C defl: list A -> list C defr: list B -> list C x: A l1: list A y: B l2: list B
map2 f defl defr (x :: l1) (y :: l2) =
f x y :: map2 f defl defr l1 l2
A, B, C: Type f: A -> B -> C defl: list A -> list C defr: list B -> list C x: A l1: list A y: B l2: list B
map2 f defl defr (x :: l1) (y :: l2) =
f x y :: map2 f defl defr l1 l2
reflexivity.Defined.(** ** Forall *)
A: Type P: A -> Type
(forallx : A, P x) -> foralll : list A, for_all P l
A: Type P: A -> Type
(forallx : A, P x) -> foralll : list A, for_all P l
intros HP l; induction l as [|x l IHl]; split; auto.Defined.
A, B: Type P: A -> Type Q: B -> Type f: A -> B Hf: forallx : A, P x -> Q (f x)
foralll : list A, for_all P l -> for_all Q (map f l)
A, B: Type P: A -> Type Q: B -> Type f: A -> B Hf: forallx : A, P x -> Q (f x)
foralll : list A, for_all P l -> for_all Q (map f l)
A, B: Type P: A -> Type Q: B -> Type f: A -> B Hf: forallx : A, P x -> Q (f x)
Unit -> Unit
A, B: Type P: A -> Type Q: B -> Type f: A -> B Hf: forallx : A, P x -> Q (f x) x: A l: list A IHl: for_all P l -> for_all Q (map f l)
P x * for_all P l -> Q (f x) * for_all Q (map f l)
A, B: Type P: A -> Type Q: B -> Type f: A -> B Hf: forallx : A, P x -> Q (f x)
Unit -> Unit
auto.
A, B: Type P: A -> Type Q: B -> Type f: A -> B Hf: forallx : A, P x -> Q (f x) x: A l: list A IHl: for_all P l -> for_all Q (map f l)
P x * for_all P l -> Q (f x) * for_all Q (map f l)
A, B: Type P: A -> Type Q: B -> Type f: A -> B Hf: forallx : A, P x -> Q (f x) x: A l: list A IHl: for_all P l -> for_all Q (map f l) Hx: P x Hl: for_all P l
Q (f x) * for_all Q (map f l)
split; auto.Defined.
A, B, C: Type P: A -> Type Q: B -> Type R: C -> Type f: A -> B -> C Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y) def_l: list A -> list C Hdefl: foralll1 : list A,
for_all P l1 -> for_all R (def_l l1) def_r: list B -> list C Hdefr: foralll2 : list B,
for_all Q l2 -> for_all R (def_r l2) l1: list A l2: list B
for_all P l1 ->
for_all Q l2 -> for_all R (map2 f def_l def_r l1 l2)
A, B, C: Type P: A -> Type Q: B -> Type R: C -> Type f: A -> B -> C Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y) def_l: list A -> list C Hdefl: foralll1 : list A,
for_all P l1 -> for_all R (def_l l1) def_r: list B -> list C Hdefr: foralll2 : list B,
for_all Q l2 -> for_all R (def_r l2) l1: list A l2: list B
for_all P l1 ->
for_all Q l2 -> for_all R (map2 f def_l def_r l1 l2)
A, B, C: Type P: A -> Type Q: B -> Type R: C -> Type f: A -> B -> C Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y) def_l: list A -> list C Hdefl: foralll1 : list A,
for_all P l1 -> for_all R (def_l l1) def_r: list B -> list C Hdefr: foralll2 : list B,
for_all Q l2 -> for_all R (def_r l2) l2: list B
for_all P nil ->
for_all Q l2 -> for_all R (map2 f def_l def_r nil l2)
A, B, C: Type P: A -> Type Q: B -> Type R: C -> Type f: A -> B -> C Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y) def_l: list A -> list C Hdefl: foralll1 : list A,
for_all P l1 -> for_all R (def_l l1) def_r: list B -> list C Hdefr: foralll2 : list B,
for_all Q l2 -> for_all R (def_r l2) x: A l1: list A l2: list B IHl1: foralll2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2)
for_all P (x :: l1) ->
for_all Q l2 ->
for_all R (map2 f def_l def_r (x :: l1) l2)
A, B, C: Type P: A -> Type Q: B -> Type R: C -> Type f: A -> B -> C Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y) def_l: list A -> list C Hdefl: foralll1 : list A,
for_all P l1 -> for_all R (def_l l1) def_r: list B -> list C Hdefr: foralll2 : list B,
for_all Q l2 -> for_all R (def_r l2) l2: list B
for_all P nil ->
for_all Q l2 -> for_all R (map2 f def_l def_r nil l2)
destruct l2 as [|y l2]; cbn; auto.
A, B, C: Type P: A -> Type Q: B -> Type R: C -> Type f: A -> B -> C Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y) def_l: list A -> list C Hdefl: foralll1 : list A,
for_all P l1 -> for_all R (def_l l1) def_r: list B -> list C Hdefr: foralll2 : list B,
for_all Q l2 -> for_all R (def_r l2) x: A l1: list A l2: list B IHl1: foralll2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2)
for_all P (x :: l1) ->
for_all Q l2 ->
for_all R (map2 f def_l def_r (x :: l1) l2)
A, B, C: Type P: A -> Type Q: B -> Type R: C -> Type f: A -> B -> C Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y) def_l: list A -> list C Hdefl: foralll1 : list A,
for_all P l1 -> for_all R (def_l l1) def_r: list B -> list C Hdefr: foralll2 : list B,
for_all Q l2 -> for_all R (def_r l2) x: A l1: list A l2: list B IHl1: foralll2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2)
P x * for_all P l1 ->
for_all Q l2 ->
for_all R
match l2 with
| nil => def_l (x :: l1)
| y :: l2 => f x y :: map2 f def_l def_r l1 l2
end
A, B, C: Type P: A -> Type Q: B -> Type R: C -> Type f: A -> B -> C Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y) def_l: list A -> list C Hdefl: foralll1 : list A,
for_all P l1 -> for_all R (def_l l1) def_r: list B -> list C Hdefr: foralll2 : list B,
for_all Q l2 -> for_all R (def_r l2) x: A l1: list A IHl1: foralll2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2) Hx: P x Hl1: for_all P l1
for_all R (def_l (x :: l1))
A, B, C: Type P: A -> Type Q: B -> Type R: C -> Type f: A -> B -> C Hf: forall (x : A) (y : B), P x -> Q y -> R (f x y) def_l: list A -> list C Hdefl: foralll1 : list A,
for_all P l1 -> for_all R (def_l l1) def_r: list B -> list C Hdefr: foralll2 : list B,
for_all Q l2 -> for_all R (def_r l2) x: A l1: list A IHl1: foralll2 : list B,
for_all P l1 ->
for_all Q l2 ->
for_all R (map2 f def_l def_r l1 l2) Hx: P x Hl1: for_all P l1
for_all P (x :: l1)
simpl; auto.Defined.
A, B: Type P: A -> Type Q: B -> Type f: A -> B -> A Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y) acc: A Ha: P acc l: list B Hl: for_all Q l
P (fold_left f l acc)
A, B: Type P: A -> Type Q: B -> Type f: A -> B -> A Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y) acc: A Ha: P acc l: list B Hl: for_all Q l
P (fold_left f l acc)
A, B: Type P: A -> Type Q: B -> Type f: A -> B -> A Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y) acc: A Ha: P acc Hl: for_all Q nil
P (fold_left f nil acc)
A, B: Type P: A -> Type Q: B -> Type f: A -> B -> A Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y) acc: A Ha: P acc x: B l: list B Hl: for_all Q (x :: l) IHl: forallacc : A, P acc -> for_all Q l -> P (fold_left f l acc)
P (fold_left f (x :: l) acc)
A, B: Type P: A -> Type Q: B -> Type f: A -> B -> A Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y) acc: A Ha: P acc Hl: for_all Q nil
P (fold_left f nil acc)
exact Ha.
A, B: Type P: A -> Type Q: B -> Type f: A -> B -> A Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y) acc: A Ha: P acc x: B l: list B Hl: for_all Q (x :: l) IHl: forallacc : A, P acc -> for_all Q l -> P (fold_left f l acc)
P (fold_left f (x :: l) acc)
A, B: Type P: A -> Type Q: B -> Type f: A -> B -> A Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y) acc: A Ha: P acc x: B l: list B Hl: for_all Q (x :: l) IHl: forallacc : A, P acc -> for_all Q l -> P (fold_left f l acc)
P (fold_left f l (f acc x))
A, B: Type P: A -> Type Q: B -> Type f: A -> B -> A Hf: forall (x : A) (y : B), P x -> Q y -> P (f x y) acc: A Ha: P acc x: B l: list B Qx: Q x Hl: for_all Q l IHl: forallacc : A, P acc -> for_all Q l -> P (fold_left f l acc)
P (fold_left f l (f acc x))
apply IHl; auto.Defined.
A: Type n: trunc_index P: A -> Type l: list A
for_all (funx : A => IsTrunc n (P x)) l ->
IsTrunc n (for_all P l)
A: Type n: trunc_index P: A -> Type l: list A
for_all (funx : A => IsTrunc n (P x)) l ->
IsTrunc n (for_all P l)
A: Type n: trunc_index P: A -> Type
Unit -> IsTrunc n Unit
A: Type n: trunc_index P: A -> Type x: A l: list A IHl: for_all (funx : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
IsTrunc n (P x) *
for_all (funx : A => IsTrunc n (P x)) l ->
IsTrunc n (P x * for_all P l)
A: Type n: trunc_index P: A -> Type
Unit -> IsTrunc n Unit
destruct n; exact _.
A: Type n: trunc_index P: A -> Type x: A l: list A IHl: for_all (funx : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l)
IsTrunc n (P x) *
for_all (funx : A => IsTrunc n (P x)) l ->
IsTrunc n (P x * for_all P l)
A: Type n: trunc_index P: A -> Type x: A l: list A IHl: for_all (funx : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l) Hx: IsTrunc n (P x) Hl: for_all (funx : A => IsTrunc n (P x)) l
IsTrunc n (P x * for_all P l)
A: Type n: trunc_index P: A -> Type x: A l: list A IHl: for_all (funx : A => IsTrunc n (P x)) l -> IsTrunc n (for_all P l) Hx: IsTrunc n (P x) Hl: IsTrunc n (for_all P l)