octalgo.octalgo.utils
Section boolUtils.
Lemma ite_id {A : Type} (b : bool) (x : A) : (if b then x else x) = x.
Lemma bool_to_prop_l (a b : bool) : (a && b) → a.
Lemma bool_to_prop_r (a b : bool) : (a && b) → b.
Lemma Eqdep_dec_bool : ∀ (b : bool) (p1 p2 : b = true), p1 = p2.
Lemma bool_des_rew (b : bool) : (b = true) ∨ (b = false).
End boolUtils.
Lemma ite_id {A : Type} (b : bool) (x : A) : (if b then x else x) = x.
Lemma bool_to_prop_l (a b : bool) : (a && b) → a.
Lemma bool_to_prop_r (a b : bool) : (a && b) → b.
Lemma Eqdep_dec_bool : ∀ (b : bool) (p1 p2 : b = true), p1 = p2.
Lemma bool_des_rew (b : bool) : (b = true) ∨ (b = false).
End boolUtils.
Section nat.
Lemma pred_ltn0_l : ∀ n m , n > 0 → n.-1 = m → n = m.+1.
Lemma ltn_leq_trans : ∀ n m p : nat, m < n → n ≤ p → m < p.
Lemma pred_ltn : ∀ n m, n.+1 < m → n < m.
Section max.
Lemma gtn_max_l : ∀ m n1 n2, (maxn n1 n2 < m) → n1 < m.
Lemma gtn_max_r : ∀ m n1 n2, (maxn n1 n2 < m) → n2 < m.
Lemma geq_max_l : ∀ m n1 n2, (maxn n1 n2 ≤ m) → n1 ≤ m.
Lemma geq_max_r : ∀ m n1 n2, (maxn n1 n2 ≤ m) → n2 ≤ m.
End max.
End nat.
Section notin.
Lemma set_notin_f_in {A : finType} (x : A) (s : {set A}) :
x \notin s = false → x \in s.
Lemma seq_notin_f_in {A : eqType} (x : A) (s : seq A) :
x \notin s = false → x \in s.
End notin.
Section finset.
Lemma iter_fun_incr {A : finType} (f g : {set A} → {set A}) (i : nat) (b : {set A}) :
[∀ x : {set A}, ∀ y : {set A}, (x \subset y) ==> (f x \subset f y)]
→ [∀ x, f x \subset g x] → iter i f b \subset iter i g b.
[∀ x : {set A}, ∀ y : {set A}, (x \subset y) ==> (f x \subset f y)]
→ [∀ x, f x \subset g x] → iter i f b \subset iter i g b.
Lemma disjointC {A : finType} (s : {set A}) : [disjoint s & ~: s].
Lemma disjoint_in_false {A : finType} (t1 t2 : {set A}) (x : A) :
x \in t1 → x \in t2 → [disjoint t1 & t2] → False.
Lemma subset_to_in {A : finType} (x : A) (s1 s2 : {set A}) : x \in s1 → s1 \subset s2 → x \in s2.
Lemma disjoint_in_false {A : finType} (t1 t2 : {set A}) (x : A) :
x \in t1 → x \in t2 → [disjoint t1 & t2] → False.
Lemma subset_to_in {A : finType} (x : A) (s1 s2 : {set A}) : x \in s1 → s1 \subset s2 → x \in s2.
Lemma equiv_part_set0 {T : finType} (P : rel T) :
equivalence_partition P set0 = set0.
Lemma equiv_part_set_mon {T : finType} (P : rel T) (s1 s2 : {set T}) :
s1 \subset s2 →
[∀ x in equivalence_partition P s1, ∃ y in equivalence_partition P s2,
x \subset y].
Lemma set0_set1_neq {A : finType} (x : A) : set0 != [set x].
Lemma not_set1P {A : finType} (x : A) (s : {set A}) :
reflect (s != [set x]) ((s == set0) || [∃ y in s, y != x]).
End finset.
Technical lemma: Folding with obind starting from None can only give None
Lemma foldObindNone {A B : Type} l (f : B → A → option A) : foldl (fun acc p ⇒ obind (f p) acc)
None l = None.
Lemma fold_maxn_n_map_geq {A : Type} {w n : nat} {l : seq A} {f : A → nat} :
(has (fun t ⇒ (w ≤ f t)) l) → w ≤ foldr maxn n (map f l).
Lemma fold_maxn_n_map_gtn {A : Type} {w n : nat} {l : seq A} {f : A → nat} :
(has (fun t ⇒ (w < f t)) l) → w < foldr maxn n (map f l).
Lemma leq_fold_maxl : ∀ l n, n ≤ foldr maxn n l.
Lemma leq_fold_base : ∀ n m l, foldr maxn n l ≤ m → n ≤ m.
Lemma foldr_maxn_base {x y m : nat} {l : seq nat} (Hyx : y ≤ x) (Hf : foldr maxn x l ≤ m) : foldr maxn y l ≤ m.
End fold.
None l = None.
Lemma fold_maxn_n_map_geq {A : Type} {w n : nat} {l : seq A} {f : A → nat} :
(has (fun t ⇒ (w ≤ f t)) l) → w ≤ foldr maxn n (map f l).
Lemma fold_maxn_n_map_gtn {A : Type} {w n : nat} {l : seq A} {f : A → nat} :
(has (fun t ⇒ (w < f t)) l) → w < foldr maxn n (map f l).
Lemma leq_fold_maxl : ∀ l n, n ≤ foldr maxn n l.
Lemma leq_fold_base : ∀ n m l, foldr maxn n l ≤ m → n ≤ m.
Lemma foldr_maxn_base {x y m : nat} {l : seq nat} (Hyx : y ≤ x) (Hf : foldr maxn x l ≤ m) : foldr maxn y l ≤ m.
End fold.
Section rem.
Lemma in_rem {A : eqType} : ∀ x h (l : seq A),
x \in l → x != h → x \in rem h l.
Lemma mem_body : ∀ (T : eqType) (s : seq T) (x y : T) , x \in s → x \in y :: s.
Lemma sub_rem {A : eqType} : ∀ (s l : seq A) h,
{subset h :: l ≤ s} → h \notin l → {subset l ≤ rem h s}.
Lemma seq_in_rem_size {A : eqType} : ∀ (h : A) s, h \in s → size s = (size (rem h s)).+1.
Lemma in_rem {A : eqType} : ∀ x h (l : seq A),
x \in l → x != h → x \in rem h l.
Lemma mem_body : ∀ (T : eqType) (s : seq T) (x y : T) , x \in s → x \in y :: s.
Lemma sub_rem {A : eqType} : ∀ (s l : seq A) h,
{subset h :: l ≤ s} → h \notin l → {subset l ≤ rem h s}.
Lemma seq_in_rem_size {A : eqType} : ∀ (h : A) s, h \in s → size s = (size (rem h s)).+1.
Lemma set_nth_notin_base {A : eqType} (x y def : A) (i : nat) :
x != def
→ x != y
→ x \notin iter i (cons def) [:: y].
Lemma set_nth_notin {A : eqType} (x y def : A) (l : seq A) (i : nat) :
x != def
→ x != y
→ x \notin l → x \notin set_nth def l i y.
Fixpoint sremove {A : Type} (s : seq A) (i : nat) : seq A :=
match i with
0 ⇒ behead s
| i.+1 ⇒ match s with
| [::] ⇒ [::]
| a::l ⇒ a::sremove l i end end.
Lemma sremove_size {A : Type} (s : seq A) (j : 'I_(size s)) :
size s = (size (sremove s j)).+1.
Lemma sremove_in_size {A : Type} (s : seq A) (j : nat) :
j < size s → size (sremove s j) = (size s).-1.
Lemma sremove_map {A B : Type} (s : seq A) (j : nat) (f : A → B) :
sremove (map f s) j = map f (sremove s j).
Lemma sremove_rem {A : eqType} (s : seq A) (j : nat) (x : A) :
find (fun y ⇒ y == x) s = j
→ j < size s
→ sremove s j = rem x s.
Lemma sremove_nth {A : eqType} (s : seq A) (j : nat) (x y : A) :
j < size s
→ sremove (set_nth x s j y) j = sremove s j.
End rem.
Section size_map_leq.
Lemma size_map_leq {A B : Type} {s : seq A} {f : A → B} {w : nat} : size s ≤ w → size (map f s) ≤ w.
Lemma pmap_size_leq {A B : Type} (f : A → option B) (s : seq A) : size (pmap f s) ≤ size s.
End size_map_leq.
Section all.
Lemma pmap_size_leq {A B : Type} (f : A → option B) (s : seq A) : size (pmap f s) ≤ size s.
End size_map_leq.
Section all.
Lemma in_nth_P {A : eqType} (def : A) (s : seq A) (P : pred A) j :
all P s → j < size s → P (nth def s j).
Lemma all_exist_seq {A B : finType} (s : seq A) P :
all (fun x ⇒ [∃ im : B, P x im]) s
→ ∃ sb,
((map fst sb) == s) && all (fun x ⇒ P (fst x) (snd x)) sb.
Lemma all_exist_enum {A B : finType} (s : {set A}) P :
[∀ x in enum s, [∃ im : B, P x im]]
→ ∃ sb,
((map fst sb) == enum s) && all (fun x ⇒ P (fst x) (snd x)) sb.
Lemma all_exist_tuple {A B : finType} (s : {set A}) P :
[∀ x in s, [∃ im : B, P x im]]
→ [∃ t : #|s|.-tuple (prod A B),
((map fst t) == enum s) && all (fun x ⇒ P (fst x) (snd x)) t].
Lemma sub_all_and_l (A : eqType) (a1 a2 : pred A) l : all (fun x ⇒ (a1 x) && a2 x) l → all a1 l.
Lemma sub_all_and_r (A : eqType) (a1 a2 : pred A) l : all (fun x ⇒ (a1 x) && a2 x) l → all a2 l.
Lemma negb_has_predC_all {A : Type} (a : pred A) (s : seq A) :
has (predC a) s = false → all a s.
End all.
Lemma pair_seq_nth_proj_l {A B : Type} (x : seq A) (k : nat) (def : (A × B)%type) (s : seq (A × B)%type) :
[seq i.1 | i <- s] = x →
(nth def s k).1 = nth def.1 x k.
Lemma map_square_eq {A B C D : Type} (f : A → C) (g : B → C) (h : A → D) (m : B → D)
(l1 : seq A) (l2 : seq B) :
(∀ x y, (f x = g y → h x = m y))
→ [seq f x | x <- l1] = [seq g y | y <- l2]
→ [seq h x | x <- l1] = [seq m y | y <- l2].
Lemma seq_inj T (x y : T) (xs ys : seq T) :
[:: x & xs] = [:: y & ys] → x = y ∧ xs = ys.
Lemma seq_in_ind {A : eqType} (def x : A) (s : seq A) :
x \in s
→ ∃ y : 'I_(size s), nth def s y = x.
Section nth_error.
Fixpoint nth_error (A : Type) (l:seq A) (n:nat) {struct n} : option A :=
match n, l with
| O, x :: _ ⇒ Some x
| S n, _ :: l ⇒ nth_error l n
| _, _ ⇒ None
end.
Lemma nth_error_in (A : eqType) (l:seq A) (n:nat) (x:A):
nth_error l n = Some x → x \in l.
Lemma nth_error_map (A B : eqType) (f: A → B) (l:seq A) (n:nat) (x:A):
nth_error l n = Some x → nth_error (map f l) n = Some (f x).
Lemma nth_error_map_none (A B : eqType) (f: A → B) (l:seq A) (n:nat):
nth_error l n = None → nth_error (map f l) n = None.
Lemma nth_error_nth (A : eqType) (l : seq A) (x def : A) (n : nat) :
nth_error l n = Some x → nth def l n = x.
Lemma nth_error_ncons1 {A : Type} (m n : nat) (x:A) :
n ≤ m
→ nth_error (ncons m x [:: x]) n = Some x.
Lemma nth_error_set_nth {A : Type} (l:seq A) (n:nat) (x:A) :
nth_error (set_nth x l n x) n = Some x.
Lemma nth_error_preim {A B : eqType} (f : A → B) (l : seq A) (y : B) (i : nat) :
nth_error (map f l) i = Some y → ∃ x : A, (nth_error l i = Some x ∧ f x = y).
Lemma nth_error_in_size {A : Type} (l : seq A) (i : nat) (x : A) :
nth_error l i = Some x → size l > i.
Lemma nth_error_notin_size {A : Type} (l : seq A) (i : nat) :
nth_error l i = None → size l ≤ i.
Lemma nth_error_size_notin {A : Type} (l : seq A) (i : nat) :
size l ≤ i → nth_error l i = None.
Lemma nth_error_sremove {A : eqType} (l : seq A) (i : nat) (x y : A) :
nth_error l i = Some x
→ x ≠ y
→ y \in l = (y \in sremove l i).
Lemma nth_error_sremove_eq {A : eqType} (l1 l2 : seq A) (i : nat) :
nth_error l1 i = nth_error l2 i
→ sremove l1 i = sremove l2 i
→ l1 = l2.
Lemma tnth_nth_error {A : Type} (l : seq A) i :
Some (tnth (in_tuple l) i) = nth_error l i.
Lemma nth_error_size_leq {A : Type} (l : seq A) i :
i < size l → ∃ x : A, nth_error l i = Some x.
Lemma oob_nth_error {A : Type} (s : seq A) (ind : 'I_(size s)) :
nth_error s ind ≠ None.
Lemma nth_error_leq_size {A : Type} (l : seq A) i :
(∃ x : A, nth_error l i = Some x) → i < size l.
Lemma nth_error_case {A : eqType} (l : seq A) (n:nat) :
nth_error l n = None ∨ ∃ x, (x \in l) ∧ nth_error l n = Some x.
Lemma nth_error_some_none_size {A B : Type} (l1 : seq A) (l2 : seq B) (x : A) (j : nat) :
nth_error l1 j = Some x → nth_error l2 j = None → size l1 = size l2 → False.
End nth_error.
Section find.
Lemma find_val {A : Type} {Q : pred A} {B : subType Q} (l : seq B) (P : pred A) :
find (fun x ⇒ P (val x)) l = find P (map val l).
Lemma nth_default_size {A : eqType} (def : A) (l : seq A) (i : nat) :
nth def l i != def → i < size l.
Lemma find_eq_nth_uniq {A : eqType} {def : A} (x : A) (l : seq A) (j : nat) :
nth def l j = x
→ x != def
→ uniq l
→ find [pred y | y == x] l = j.
Lemma find_iota i k :
k < i
→ find [pred x | x == k] (iota 0 i) = k.
End find.
End seq.
Fixpoint nth_error (A : Type) (l:seq A) (n:nat) {struct n} : option A :=
match n, l with
| O, x :: _ ⇒ Some x
| S n, _ :: l ⇒ nth_error l n
| _, _ ⇒ None
end.
Lemma nth_error_in (A : eqType) (l:seq A) (n:nat) (x:A):
nth_error l n = Some x → x \in l.
Lemma nth_error_map (A B : eqType) (f: A → B) (l:seq A) (n:nat) (x:A):
nth_error l n = Some x → nth_error (map f l) n = Some (f x).
Lemma nth_error_map_none (A B : eqType) (f: A → B) (l:seq A) (n:nat):
nth_error l n = None → nth_error (map f l) n = None.
Lemma nth_error_nth (A : eqType) (l : seq A) (x def : A) (n : nat) :
nth_error l n = Some x → nth def l n = x.
Lemma nth_error_ncons1 {A : Type} (m n : nat) (x:A) :
n ≤ m
→ nth_error (ncons m x [:: x]) n = Some x.
Lemma nth_error_set_nth {A : Type} (l:seq A) (n:nat) (x:A) :
nth_error (set_nth x l n x) n = Some x.
Lemma nth_error_preim {A B : eqType} (f : A → B) (l : seq A) (y : B) (i : nat) :
nth_error (map f l) i = Some y → ∃ x : A, (nth_error l i = Some x ∧ f x = y).
Lemma nth_error_in_size {A : Type} (l : seq A) (i : nat) (x : A) :
nth_error l i = Some x → size l > i.
Lemma nth_error_notin_size {A : Type} (l : seq A) (i : nat) :
nth_error l i = None → size l ≤ i.
Lemma nth_error_size_notin {A : Type} (l : seq A) (i : nat) :
size l ≤ i → nth_error l i = None.
Lemma nth_error_sremove {A : eqType} (l : seq A) (i : nat) (x y : A) :
nth_error l i = Some x
→ x ≠ y
→ y \in l = (y \in sremove l i).
Lemma nth_error_sremove_eq {A : eqType} (l1 l2 : seq A) (i : nat) :
nth_error l1 i = nth_error l2 i
→ sremove l1 i = sremove l2 i
→ l1 = l2.
Lemma tnth_nth_error {A : Type} (l : seq A) i :
Some (tnth (in_tuple l) i) = nth_error l i.
Lemma nth_error_size_leq {A : Type} (l : seq A) i :
i < size l → ∃ x : A, nth_error l i = Some x.
Lemma oob_nth_error {A : Type} (s : seq A) (ind : 'I_(size s)) :
nth_error s ind ≠ None.
Lemma nth_error_leq_size {A : Type} (l : seq A) i :
(∃ x : A, nth_error l i = Some x) → i < size l.
Lemma nth_error_case {A : eqType} (l : seq A) (n:nat) :
nth_error l n = None ∨ ∃ x, (x \in l) ∧ nth_error l n = Some x.
Lemma nth_error_some_none_size {A B : Type} (l1 : seq A) (l2 : seq B) (x : A) (j : nat) :
nth_error l1 j = Some x → nth_error l2 j = None → size l1 = size l2 → False.
End nth_error.
Section find.
Lemma find_val {A : Type} {Q : pred A} {B : subType Q} (l : seq B) (P : pred A) :
find (fun x ⇒ P (val x)) l = find P (map val l).
Lemma nth_default_size {A : eqType} (def : A) (l : seq A) (i : nat) :
nth def l i != def → i < size l.
Lemma find_eq_nth_uniq {A : eqType} {def : A} (x : A) (l : seq A) (j : nat) :
nth def l j = x
→ x != def
→ uniq l
→ find [pred y | y == x] l = j.
Lemma find_iota i k :
k < i
→ find [pred x | x == k] (iota 0 i) = k.
End find.
End seq.
Definition dep_iota (m n : nat) : seq ('I_(m+n)) :=
pmap insub (iota m n).
Lemma dep_iotaE (m n : nat) : map val (dep_iota m n) = iota m n.
Lemma dep_iota_uniq (m n : nat) : uniq (dep_iota m n).
Lemma size_dep_iota (m n : nat) : size (dep_iota m n) = n.
Definition equip (T : finType) (P : pred T) (A : {set T}) : {set {x : T | P x}} :=
[set x in pmap insub (enum A)].
[set x in pmap insub (enum A)].
Section bigop.
Lemma bigcup_type_seq {A B : finType} {f : A → {set B}} : ∀ (x : B) z,
x \in \bigcup_(y <- z) f y → x \in \bigcup_y f y.
End bigop.
Section Prod.
Lemma prod_eq {A B : Type} (x y : prod A B) : fst x = fst y → snd x = snd y → x = y.
End Prod.
Lemma bigcup_type_seq {A B : finType} {f : A → {set B}} : ∀ (x : B) z,
x \in \bigcup_(y <- z) f y → x \in \bigcup_y f y.
End bigop.
Section Prod.
Lemma prod_eq {A B : Type} (x y : prod A B) : fst x = fst y → snd x = snd y → x = y.
End Prod.
Section ord.
Lemma ord_shiftl {i : nat} : ∀ x : 'I_i, x.+1 < i.+1.
Definition ord_shift {i : nat} (x : 'I_i) : 'I_i.+1 :=
Ordinal (ord_shiftl x).
Definition shift {i j : nat} (l : j.-tuple 'I_i) : j.-tuple 'I_(i.+1) :=
[tuple of (map (fun (x : 'I_i) ⇒ ord_shift x) l)].
End ord.
Definition pimset {A B : finType} (f : A → option B) (s : {set A}) : {set B} :=
[set id x | x in (pmap f [seq y | y in s])].
Definition pset {A : finType} (s : {set (option A)}) : {set A} := pimset id s.
Lemma mem_set_pset {A : finType} (x : A) (s : {set (option A)}) : Some x \in s → x \in pset s.
Lemma mem_pset_set {A : finType} (x : A) (s : {set (option A)}) : x \in pset s → Some x \in s.
Section all_prop.
Fixpoint all_prop (T : Type) (a : T → Prop) (s : seq T) := match s with
| [::] ⇒ True
| x::s' ⇒ a x ∧ all_prop a s' end.
Lemma all_prop_cat_l {A : Type} {P : A → Prop} {l l' : seq A} (H : all_prop P (l ++ l')) : all_prop P l.
Lemma all_prop_cat_r {A : Type} {P : A → Prop} {l l' : seq A} (H : all_prop P (l ++ l')) : all_prop P l'.
Lemma all_prop_cat {A : Type} {P : A → Prop} {l l' : seq A} :
all_prop P (l ++ l') ↔ all_prop P l ∧ all_prop P l'.
Lemma all_prop_in {A : eqType} {P : A → Prop} {l : seq A} {x : A}
(Hp : all_prop P l) (Hin : x \in l) : P x.
Lemma all_prop_seq_decr {A : eqType} {P : A → Prop}:
∀ l1 l2, all_prop P l2 → {subset l1 ≤ l2} → all_prop P l1.
Lemma all_prop_prop_decr {A : eqType} (a1 a2 : A → Prop) (s : seq A) :
(all_prop a1 s) → (∀ x, x \in s → a1 x → a2 x) → all_prop a2 s.
Lemma fold_maxn_n_map_leq {A : Type} {w n : nat} {l : seq A} {f : A → nat} :
n ≤ w → (all_prop (fun t ⇒ (f t ≤ w)) l) → foldr maxn n (map f l) ≤ w.
Lemma fold_maxn_n_map_ltn {A : Type} {w n : nat} {l : seq A} {f : A → nat} :
n < w → (all_prop (fun t ⇒ (f t < w)) l) → foldr maxn n (map f l) < w.
Lemma sub_rem_seq {A : eqType} : ∀ (l : seq (seq A)) s h,
all_prop (fun x : seq A ⇒ {subset x ≤ s}) [seq h :: i | i <- l] →
all_prop (fun sl ⇒ h \notin sl) l →
all_prop (fun x : seq_predType A ⇒ {subset x ≤ rem h s}) l.
Lemma sub_val_map (A : eqType) (P : pred A) (B : subType P) (l : seq A)
(ls : seq B) (Heq : l = map val ls) :
all_prop (fun x : A ⇒ ∃ px : P x, @Sub A P B x px \in ls) l.
End all_prop.
Fixpoint all_prop (T : Type) (a : T → Prop) (s : seq T) := match s with
| [::] ⇒ True
| x::s' ⇒ a x ∧ all_prop a s' end.
Lemma all_prop_cat_l {A : Type} {P : A → Prop} {l l' : seq A} (H : all_prop P (l ++ l')) : all_prop P l.
Lemma all_prop_cat_r {A : Type} {P : A → Prop} {l l' : seq A} (H : all_prop P (l ++ l')) : all_prop P l'.
Lemma all_prop_cat {A : Type} {P : A → Prop} {l l' : seq A} :
all_prop P (l ++ l') ↔ all_prop P l ∧ all_prop P l'.
Lemma all_prop_in {A : eqType} {P : A → Prop} {l : seq A} {x : A}
(Hp : all_prop P l) (Hin : x \in l) : P x.
Lemma all_prop_seq_decr {A : eqType} {P : A → Prop}:
∀ l1 l2, all_prop P l2 → {subset l1 ≤ l2} → all_prop P l1.
Lemma all_prop_prop_decr {A : eqType} (a1 a2 : A → Prop) (s : seq A) :
(all_prop a1 s) → (∀ x, x \in s → a1 x → a2 x) → all_prop a2 s.
Lemma fold_maxn_n_map_leq {A : Type} {w n : nat} {l : seq A} {f : A → nat} :
n ≤ w → (all_prop (fun t ⇒ (f t ≤ w)) l) → foldr maxn n (map f l) ≤ w.
Lemma fold_maxn_n_map_ltn {A : Type} {w n : nat} {l : seq A} {f : A → nat} :
n < w → (all_prop (fun t ⇒ (f t < w)) l) → foldr maxn n (map f l) < w.
Lemma sub_rem_seq {A : eqType} : ∀ (l : seq (seq A)) s h,
all_prop (fun x : seq A ⇒ {subset x ≤ s}) [seq h :: i | i <- l] →
all_prop (fun sl ⇒ h \notin sl) l →
all_prop (fun x : seq_predType A ⇒ {subset x ≤ rem h s}) l.
Lemma sub_val_map (A : eqType) (P : pred A) (B : subType P) (l : seq A)
(ls : seq B) (Heq : l = map val ls) :
all_prop (fun x : A ⇒ ∃ px : P x, @Sub A P B x px \in ls) l.
End all_prop.