:: Coincidence Lemma and Substitution Lemma
::  by Patrick Braselmann and Peter Koepke
::
:: Received September 25, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies SUBSET_1, NUMBERS, CQC_LANG, QC_LANG1, XBOOLE_0, VALUAT_1,
      FUNCT_1, FINSEQ_1, RELAT_1, TARSKI, FUNCT_4, FUNCOP_1, PARTFUN1, FUNCT_2,
      MCART_1, REALSET1, XBOOLEAN, ZF_MODEL, ORDINAL4, ZF_LANG, ARYTM_3, NAT_1,
      XXREAL_0, ZFMISC_1, BVFUNC_2, CLASSES2, ZF_LANG1, SUBLEMMA, CARD_1,
      SUBSTUT1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, FINSEQ_1, FUNCT_1,
      ORDINAL1, NAT_1, QC_LANG1, QC_LANG3, PARTFUN1, CARD_1, NUMBERS, XXREAL_0,
      FUNCOP_1, CQC_LANG, RELAT_1, FUNCT_4, SEQ_4, VALUAT_1, RELSET_1, FUNCT_2,
      MARGREL1, DOMAIN_1, MCART_1, SUBSTUT1;
 constructors DOMAIN_1, FUNCT_4, XXREAL_0, SEQ_4, QC_LANG3, VALUAT_1, RELSET_1,
      SUBSTUT1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      QC_LANG1, CQC_LANG, XXREAL_0, RELSET_1, SUBSTUT1, FUNCT_4, XTUPLE_0;
 requirements NUMERALS, SUBSET, BOOLE;


begin :: Preliminaries

reserve Al for QC-alphabet;
reserve a,b,c,d for object,
  i,k,n for Nat,
  p,q for Element of CQC-WFF(Al),
  x,y,y1 for bound_QC-variable of Al,
  A for non empty set,
  J for interpretation of Al,A,
  v,w for Element of Valuations_in(Al,A),
  f,g for Function,
  P,P9 for QC-pred_symbol of k,Al,
  ll,ll9 for CQC-variable_list of k,Al,
  l1 for FinSequence of QC-variables(Al),
  Sub,Sub9,Sub1 for CQC_Substitution of Al,
  S,S9,S1,S2 for Element of CQC-Sub-WFF(Al),
  s for QC-symbol of Al;

theorem :: SUBLEMMA:1
  for f,g,h,h1,h2 being Function st dom h1 c= dom h & dom h2 c= dom
  h holds f+*g+*h = (f+*h1)+*(g+*h2)+*h;

theorem :: SUBLEMMA:2
  for vS1 being Function st x in dom vS1 holds (vS1|((dom vS1) \ {x
  })) +* (x .--> vS1.x) = vS1;

definition
  let Al,A;
  mode Val_Sub of A,Al is PartFunc of bound_QC-variables(Al),A;
end;

reserve vS,vS1,vS2 for Val_Sub of A,Al;

notation
  let Al, A, v, vS;
  synonym v.vS for v +* vS;
end;

definition
  let Al, A, v, vS;
  redefine func v.vS -> Element of Valuations_in(Al,A);
end;

definition
  let Al,S;
  redefine func S`1 -> Element of CQC-WFF(Al);
end;

definition
  let Al, S, A, v;
  func Val_S(v,S) -> Val_Sub of A,Al equals
:: SUBLEMMA:def 1
  (@S`2)*v;
end;

theorem :: SUBLEMMA:3
  S is Al-Sub_VERUM implies CQC_Sub(S) = VERUM(Al);

definition
  let Al, S, A, v, J;
  pred J,v |= S means
:: SUBLEMMA:def 2

  J,v |= S`1;
end;

theorem :: SUBLEMMA:4
  S is Al-Sub_VERUM implies for v holds (J,v |= CQC_Sub(S) iff J,v.
  Val_S(v,S) |= S);

theorem :: SUBLEMMA:5
  i in dom ll implies ll.i is bound_QC-variable of Al;

theorem :: SUBLEMMA:6
  S is Sub_atomic implies CQC_Sub(S) = (the_pred_symbol_of S`1)!
  CQC_Subst(Sub_the_arguments_of S,S`2);

theorem :: SUBLEMMA:7
  Sub_the_arguments_of Sub_P(P,ll,Sub) = Sub_the_arguments_of Sub_P(P9,
  ll9,Sub9) implies ll = ll9;

definition
  let k, Al, P, ll, Sub;
  redefine func Sub_P(P,ll,Sub) -> Element of CQC-Sub-WFF(Al);
end;

theorem :: SUBLEMMA:8
  CQC_Sub(Sub_P(P,ll,Sub)) = P!CQC_Subst(ll,Sub);

theorem :: SUBLEMMA:9
  P!CQC_Subst(ll,Sub) is Element of CQC-WFF(Al);

theorem :: SUBLEMMA:10
  CQC_Subst(ll,Sub) is CQC-variable_list of k,Al;

registration
  let Al;
  let k, ll, Sub;
  cluster CQC_Subst(ll,Sub) -> bound_QC-variables(Al) -valued k-element;
end;

theorem :: SUBLEMMA:11
  not x in dom S`2 implies (v.Val_S(v,S)).x = v.x;

theorem :: SUBLEMMA:12
  x in dom S`2 implies (v.Val_S(v,S)).x = Val_S(v,S).x;

theorem :: SUBLEMMA:13
  (v.Val_S(v,Sub_P(P,ll,Sub)))*'ll = v*'(CQC_Subst(ll,Sub));

theorem :: SUBLEMMA:14
  Sub_P(P,ll,Sub)`1 = P!ll;

theorem :: SUBLEMMA:15
  for v holds (J,v |= CQC_Sub(Sub_P(P,ll,Sub)) iff J,v.Val_S(v,
  Sub_P(P,ll,Sub)) |= Sub_P(P,ll,Sub));

theorem :: SUBLEMMA:16
  (Sub_not S)`1 = 'not' S`1 & (Sub_not S)`2 = S`2;

definition
  let Al,S;
  redefine func Sub_not S -> Element of CQC-Sub-WFF(Al);
end;

theorem :: SUBLEMMA:17
  not J,v.Val_S(v,S) |= S iff J,v.Val_S(v,S) |= Sub_not S;

theorem :: SUBLEMMA:18
  Val_S(v,S) = Val_S(v,Sub_not S);

theorem :: SUBLEMMA:19
  (for v holds (J,v |= CQC_Sub(S) iff J,v.Val_S(v,S) |= S))
  implies for v holds (J,v |= CQC_Sub(Sub_not S) iff J,v.Val_S(v,Sub_not S) |=
  Sub_not S);

definition
  let Al, S1, S2;
  assume
 S1`2 = S2`2;
  func CQCSub_&(S1,S2) -> Element of CQC-Sub-WFF(Al) equals
:: SUBLEMMA:def 3

  Sub_&(S1,S2);
end;

theorem :: SUBLEMMA:20
  S1`2 = S2`2 implies CQCSub_&(S1,S2)`1 = (S1`1) '&' (S2`1) &
  CQCSub_&(S1,S2)`2 = S1`2;

theorem :: SUBLEMMA:21
  S1`2 = S2`2 implies CQCSub_&(S1,S2)`2 = S1`2;

theorem :: SUBLEMMA:22
  S1`2 = S2`2 implies Val_S(v,S1) = Val_S(v,CQCSub_&(S1,S2)) & Val_S(v,
  S2) = Val_S(v,CQCSub_&(S1,S2));

theorem :: SUBLEMMA:23
  S1`2 = S2`2 implies CQC_Sub(CQCSub_&(S1,S2)) = (CQC_Sub(S1)) '&'
  (CQC_Sub(S2));

theorem :: SUBLEMMA:24
  S1`2 = S2`2 implies (J,v.Val_S(v,S1) |= S1 & J,v.Val_S(v,S2) |=
  S2 iff J,v.Val_S(v,CQCSub_&(S1,S2)) |= CQCSub_&(S1,S2));

theorem :: SUBLEMMA:25
  S1`2 = S2`2 & (for v holds (J,v |= CQC_Sub(S1) iff J,v.Val_S(v,
  S1) |= S1)) & (for v holds (J,v |= CQC_Sub(S2) iff J,v.Val_S(v,S2) |= S2))
implies for v holds (J,v |= CQC_Sub(CQCSub_&(S1,S2)) iff J,v.Val_S(v,CQCSub_&(
  S1,S2)) |= CQCSub_&(S1,S2));

reserve B for Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):],
  SQ for second_Q_comp of B;

theorem :: SUBLEMMA:26
  B is quantifiable implies Sub_All(B,SQ)`1 = All(B`2,(B`1)`1) &
  Sub_All(B,SQ)`2 = SQ;

definition
  let Al;
  let B be Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):];
  attr B is CQC-WFF-like means
:: SUBLEMMA:def 4

  B`1 in CQC-Sub-WFF(Al);
end;

registration
  let Al;
  cluster CQC-WFF-like for Element of [:QC-Sub-WFF(Al),
   bound_QC-variables(Al):];
end;

definition
  let Al, S, x;
  redefine func [S,x] -> CQC-WFF-like Element of [:QC-Sub-WFF(Al),
  bound_QC-variables(Al):];
end;

reserve B for CQC-WFF-like Element of [:QC-Sub-WFF(Al),
  bound_QC-variables(Al):],
  xSQ for second_Q_comp of [S,x],
  SQ for second_Q_comp of B;

definition
  let Al, B;
  redefine func B`1 -> Element of CQC-Sub-WFF(Al);
end;

definition
  let Al, B, SQ;
  assume
 B is quantifiable;
  func CQCSub_All(B,SQ) -> Element of CQC-Sub-WFF(Al) equals
:: SUBLEMMA:def 5

  Sub_All(B,SQ);
end;

theorem :: SUBLEMMA:27
  B is quantifiable implies CQCSub_All(B,SQ) is Sub_universal;

definition
  let Al;
  let S such that
 S is Sub_universal;
  func CQCSub_the_scope_of S -> Element of CQC-Sub-WFF(Al) equals
:: SUBLEMMA:def 6

  Sub_the_scope_of S;
end;

definition
  let Al, S1, p;
  assume that
 S1 is Sub_universal and
 p = CQC_Sub(CQCSub_the_scope_of S1);
  func CQCQuant(S1,p) -> Element of CQC-WFF(Al) equals
:: SUBLEMMA:def 7

  Quant(S1,p);
end;

theorem :: SUBLEMMA:28
  S is Sub_universal implies CQC_Sub(S) = CQCQuant(S,CQC_Sub(
  CQCSub_the_scope_of S));

theorem :: SUBLEMMA:29
  B is quantifiable implies CQCSub_the_scope_of(CQCSub_All(B,SQ)) = B`1;

begin :: The Substitution Lemma

theorem :: SUBLEMMA:30
  [S,x] is quantifiable implies CQCSub_the_scope_of(CQCSub_All([S,
  x],xSQ)) = S & CQCQuant(CQCSub_All([S,x],xSQ),CQC_Sub(CQCSub_the_scope_of
  CQCSub_All([S,x],xSQ))) = CQCQuant(CQCSub_All([S,x],xSQ),CQC_Sub(S));

theorem :: SUBLEMMA:31
  [S,x] is quantifiable implies CQCQuant(CQCSub_All([S,x],xSQ),
  CQC_Sub(S)) = All(S_Bound(@CQCSub_All([S,x],xSQ)),CQC_Sub(S));

theorem :: SUBLEMMA:32
  x in dom S`2 implies v.((@S`2).x) = v.Val_S(v,S).x;

theorem :: SUBLEMMA:33
  x in dom (@S`2) implies (@S`2).x is bound_QC-variable of Al;

theorem :: SUBLEMMA:34
  [:QC-WFF(Al),vSUB(Al):] c= dom QSub(Al);

reserve B1 for Element of [:QC-Sub-WFF(Al),bound_QC-variables(Al):];
reserve SQ1 for second_Q_comp of B1;

theorem :: SUBLEMMA:35
  B is quantifiable & B1 is quantifiable & Sub_All(B,SQ) = Sub_All
  (B1,SQ1) implies B`2 = B1`2 & SQ = SQ1;

theorem :: SUBLEMMA:36
  B is quantifiable & B1 is quantifiable & CQCSub_All(B,SQ) =
  Sub_All(B1,SQ1) implies B`2 = B1`2 & SQ = SQ1;

theorem :: SUBLEMMA:37
  [S,x] is quantifiable implies Sub_the_bound_of CQCSub_All([S,x],xSQ) = x;

theorem :: SUBLEMMA:38
  [S,x] is quantifiable & x in rng RestrictSub(x,All(x,S`1),xSQ)
implies not S_Bound(@CQCSub_All([S,x],xSQ)) in rng RestrictSub(x,All(x,S`1),xSQ
  ) & not S_Bound(@CQCSub_All([S,x],xSQ)) in Bound_Vars(S`1);

theorem :: SUBLEMMA:39
  [S,x] is quantifiable & not x in rng RestrictSub(x,All(x,S`1),
xSQ) implies not S_Bound(@CQCSub_All([S,x],xSQ)) in rng RestrictSub(x,All(x,S`1
  ),xSQ);

theorem :: SUBLEMMA:40
  [S,x] is quantifiable implies not S_Bound(@CQCSub_All([S,x],xSQ)
  ) in rng RestrictSub(x,All(x,S`1),xSQ);

theorem :: SUBLEMMA:41
  [S,x] is quantifiable implies S`2 = ExpandSub(x,S`1,RestrictSub(
  x,All(x,S`1),xSQ));

theorem :: SUBLEMMA:42
  still_not-bound_in VERUM(Al) c= Bound_Vars(VERUM(Al));

theorem :: SUBLEMMA:43
  still_not-bound_in (P!ll) = Bound_Vars(P!ll);

theorem :: SUBLEMMA:44
  still_not-bound_in (p) c= Bound_Vars(p) implies
  still_not-bound_in ('not' p) c= Bound_Vars('not' p);

theorem :: SUBLEMMA:45
  still_not-bound_in p c= Bound_Vars(p) & still_not-bound_in q c=
  Bound_Vars(q) implies still_not-bound_in (p '&' q) c= Bound_Vars(p '&' q);

theorem :: SUBLEMMA:46
  still_not-bound_in p c= Bound_Vars(p) implies still_not-bound_in
  All(x,p) c= Bound_Vars(All(x,p));

theorem :: SUBLEMMA:47
  for p holds still_not-bound_in p c= Bound_Vars(p);

notation
  let Al, A, x;
  let a be Element of A;
  synonym x|a for x .--> a;
end;

definition
  let Al, A, x;
  let a be Element of A;
  redefine func x|a -> Val_Sub of A,Al;
end;

reserve a for Element of A;

theorem :: SUBLEMMA:48
  x <> b implies v.(x|a).b = v.b;

theorem :: SUBLEMMA:49
  x = y implies v.(x|a).y = a;

theorem :: SUBLEMMA:50
  J,v |= All(x,p) iff for a holds J,v.(x|a) |= p;

definition
  let Al, S, x, xSQ, A, v;
  func NEx_Val(v,S,x,xSQ) -> Val_Sub of A,Al equals
:: SUBLEMMA:def 8
  (@RestrictSub(x,All(x,S`1),
  xSQ))*v;
end;

definition
  let Al, A;
  let v,w be Val_Sub of A,Al;
  redefine func v+*w -> Val_Sub of A,Al;
end;

theorem :: SUBLEMMA:51
  [S,x] is quantifiable & x in rng RestrictSub(x,All(x,S`1),xSQ)
implies S_Bound(@CQCSub_All([S,x],xSQ)) = x.upVar(RestrictSub(x,All(x,S`1),xSQ)
  ,S`1);

theorem :: SUBLEMMA:52
  [S,x] is quantifiable & not x in rng RestrictSub(x,All(x,S`1),
  xSQ) implies S_Bound(@CQCSub_All([S,x],xSQ)) = x;

theorem :: SUBLEMMA:53
  [S,x] is quantifiable implies for a holds Val_S(v.((S_Bound(@
CQCSub_All([S,x],xSQ)))|a),S) = NEx_Val(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a)
  ,S,x,xSQ)+*(x|a) & dom RestrictSub(x,All(x,S`1),xSQ) misses {x};

theorem :: SUBLEMMA:54
  [S,x] is quantifiable implies ((for a holds J,(v.((S_Bound(@
  CQCSub_All([S,x],xSQ)))|a)). Val_S(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a),S)
|= S) iff for a holds J,(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a)). (NEx_Val(v.(
  (S_Bound(@CQCSub_All([S,x],xSQ)))|a),S,x,xSQ)+*(x|a)) |= S);

theorem :: SUBLEMMA:55
  [S,x] is quantifiable implies for a holds NEx_Val(v.((S_Bound(@
  CQCSub_All([S,x],xSQ)))|a),S,x,xSQ) = NEx_Val(v,S,x,xSQ);

theorem :: SUBLEMMA:56
  [S,x] is quantifiable implies ((for a holds J,(v.((S_Bound(@
CQCSub_All([S,x],xSQ)))|a)). (NEx_Val(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a),S
,x,xSQ)+*(x|a)) |= S) iff for a holds J,(v.((S_Bound(@CQCSub_All([S,x],xSQ)))|a
  )). (NEx_Val(v,S,x,xSQ)+*(x|a)) |= S );

begin :: The Coincidence Lemma

theorem :: SUBLEMMA:57
  rng l1 c= bound_QC-variables(Al) implies still_not-bound_in l1 = rng l1;

theorem :: SUBLEMMA:58
  dom v = bound_QC-variables(Al) & dom (x|a) = {x};

theorem :: SUBLEMMA:59
  v*'ll = ll*(v|still_not-bound_in ll);

theorem :: SUBLEMMA:60
  for v,w holds (v|still_not-bound_in (P!ll) = w|
  still_not-bound_in (P!ll) implies (J,v |= P!ll iff J,w |= P!ll));

theorem :: SUBLEMMA:61
  (for v,w holds v|still_not-bound_in p = w|still_not-bound_in p
  implies (J,v |= p iff J,w |= p)) implies for v,w holds v|still_not-bound_in
'not' p = w|still_not-bound_in 'not' p implies (J,v |= 'not' p iff J,w |= 'not'
  p);

theorem :: SUBLEMMA:62
  (for v,w holds v|still_not-bound_in p = w|still_not-bound_in p
  implies (J,v |= p iff J,w |= p)) & (for v,w holds v|still_not-bound_in q = w|
still_not-bound_in q implies (J,v |= q iff J,w |= q)) implies for v,w holds v|
still_not-bound_in p '&' q = w|still_not-bound_in p '&' q implies (J,v |= p '&'
  q iff J,w |= p '&' q);

theorem :: SUBLEMMA:63
  for X being set st X c= bound_QC-variables(Al) holds dom (v|X) = dom
  (v.(x|a)|X) & dom (v|X) = X;

theorem :: SUBLEMMA:64
  v|still_not-bound_in p = w|still_not-bound_in p implies v.(x|a)|
  still_not-bound_in p = w.(x|a)|still_not-bound_in p;

theorem :: SUBLEMMA:65
  still_not-bound_in p c= still_not-bound_in (All(x,p)) \/ {x};

theorem :: SUBLEMMA:66
  v|(still_not-bound_in p \ {x}) = w|(still_not-bound_in p \ {x})
  implies v.(x|a)|still_not-bound_in p = w.(x|a)|still_not-bound_in p;

theorem :: SUBLEMMA:67
  (for v,w holds v|still_not-bound_in p = w|still_not-bound_in p
implies (J,v |= p iff J,w |= p)) implies for v,w holds v|still_not-bound_in All
(x,p) = w|still_not-bound_in All(x,p) implies (J,v |= All(x,p) iff J,w |= All(x
  ,p));

:: Coincidence Lemma (Ebb et al, Chapter III, 5.1)

theorem :: SUBLEMMA:68
  for p holds for v,w holds v|still_not-bound_in p = w|
  still_not-bound_in p implies (J,v |= p iff J,w |= p);

theorem :: SUBLEMMA:69
  [S,x] is quantifiable implies (v.((S_Bound(@CQCSub_All([S,x],xSQ
)))|a)). (NEx_Val(v,S,x,xSQ)+*(x|a))|still_not-bound_in S`1 = (v.(NEx_Val(v,S,x
  ,xSQ)+*(x|a)))|still_not-bound_in S`1;

theorem :: SUBLEMMA:70
  [S,x] is quantifiable implies ((for a holds J,(v.((S_Bound(@
CQCSub_All([S,x],xSQ)))|a)).(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S) iff for a holds J
  ,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S );

theorem :: SUBLEMMA:71
  dom NEx_Val(v,S,x,xSQ) = dom RestrictSub(x,All(x,S`1),xSQ);

theorem :: SUBLEMMA:72
  (for a holds J,v.(NEx_Val(v,S,x,xSQ)+*(x|a)) |= S) iff for a
  holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S;

theorem :: SUBLEMMA:73
  (for a holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S) iff for a
  holds J,(v.NEx_Val(v,S,x,xSQ)).(x|a) |= S`1;

theorem :: SUBLEMMA:74
  for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
  still_not-bound_in ll) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
  misses dom vS2 holds (v.vS)*'ll = (v.(vS+*vS1+*vS2))*'ll;

theorem :: SUBLEMMA:75
  for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
still_not-bound_in (P!ll)) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
  misses dom vS2 holds J,v.vS |= P!ll iff J,v.(vS+*vS1+*vS2) |= P!ll;

theorem :: SUBLEMMA:76
  (for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
  still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p) implies for v,vS,
vS1,vS2 st (for y st y in dom vS1 holds not y in still_not-bound_in 'not' p) &
(for y st y in dom vS2 holds vS2.y = v.y) & dom vS misses dom vS2 holds J,v.vS
  |= 'not' p iff J,v.(vS+*vS1+*vS2) |= 'not' p;

theorem :: SUBLEMMA:77
  (for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
  still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p) & (for v,vS,vS1,
vS2 st (for y st y in dom vS1 holds not y in still_not-bound_in q) & (for y st
y in dom vS2 holds vS2.y = v.y) & dom vS misses dom vS2 holds J,v.vS |= q iff J
  ,v.(vS+*vS1+*vS2) |= q) implies for v,vS,vS1,vS2 st (for y st y in dom vS1
holds not y in still_not-bound_in p '&' q) & (for y st y in dom vS2 holds vS2.y
  = v.y) & dom vS misses dom vS2 holds J,v.vS |= p '&' q iff J,v.(vS+*vS1+*vS2)
  |= p '&' q;

theorem :: SUBLEMMA:78
  (for y st y in dom vS1 holds not y in still_not-bound_in All(x,p
  )) implies for y st y in (dom vS1) \ {x} holds not y in still_not-bound_in p;

theorem :: SUBLEMMA:79
  for vS1 being Function holds (for y st y in dom vS1 holds vS1.y
= v.y) & dom vS misses dom vS1 implies for y st y in (dom vS1) \ {x} holds vS1|
  ((dom vS1) \ {x}).y = (v.vS).y;

theorem :: SUBLEMMA:80
  (for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not y in
  still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p) implies for v,vS,
vS1,vS2 st (for y st y in dom vS1 holds not y in still_not-bound_in All(x,p)) &
(for y st y in dom vS2 holds vS2.y = v.y) & dom vS misses dom vS2 holds J,v.vS
  |= All(x,p) iff J,v.(vS+*vS1+*vS2) |= All(x,p);

theorem :: SUBLEMMA:81
  for p holds for v,vS,vS1,vS2 st (for y st y in dom vS1 holds not
y in still_not-bound_in p) & (for y st y in dom vS2 holds vS2.y = v.y) & dom vS
  misses dom vS2 holds J,v.vS |= p iff J,v.(vS+*vS1+*vS2) |= p;

definition
  let Al, p;
  func RSub1(p) -> set means
:: SUBLEMMA:def 9

  b in it iff ex x st x = b & not x in still_not-bound_in p;
end;

definition
  let Al, p, Sub;
  func RSub2(p,Sub) -> set means
:: SUBLEMMA:def 10

  b in it iff ex x st x = b & x in still_not-bound_in p & x = (@Sub).x;
end;

theorem :: SUBLEMMA:82
  dom ((@Sub)|RSub1(p)) misses dom ((@Sub)|RSub2(p,Sub));

theorem :: SUBLEMMA:83
  @RestrictSub(x,All(x,p),Sub) = @Sub \ ((@Sub)|RSub1(All(x,p)) +*
  (@Sub)|RSub2(All(x,p),Sub));

theorem :: SUBLEMMA:84
  dom @RestrictSub(x,p,Sub) misses dom ((@Sub)|RSub1(p)) \/ dom ((
  @Sub)|RSub2(p,Sub));

theorem :: SUBLEMMA:85
  [S,x] is quantifiable implies @(CQCSub_All([S,x],xSQ))`2 = @
RestrictSub(x,All(x,S`1),xSQ) +* (@xSQ)|RSub1(All(x,S`1)) +* (@xSQ)|RSub2(All(x
  ,S`1),xSQ);

theorem :: SUBLEMMA:86
  [S,x] is quantifiable implies ex vS1,vS2 st (for y st y in dom
  vS1 holds not y in still_not-bound_in All(x,S`1)) & (for y st y in dom vS2
  holds vS2.y = v.y) & dom NEx_Val(v,S,x,xSQ) misses dom vS2 & v.Val_S(v,
  CQCSub_All([S,x],xSQ)) = v.(NEx_Val(v,S,x,xSQ) +* vS1 +* vS2);

theorem :: SUBLEMMA:87
  [S,x] is quantifiable implies for v holds (J,v.NEx_Val(v,S,x,xSQ
) |= All(x,S`1) iff J,v.Val_S(v,CQCSub_All([S,x],xSQ)) |= CQCSub_All([S,x],xSQ)
  );

theorem :: SUBLEMMA:88
  [S,x] is quantifiable & (for v holds (J,v |= CQC_Sub(S) iff J,v.
  Val_S(v,S) |= S)) implies for v holds (J,v |= CQC_Sub(CQCSub_All([S,x],xSQ))
  iff J,v.Val_S(v,CQCSub_All([S,x],xSQ)) |= CQCSub_All([S,x],xSQ));

scheme :: SUBLEMMA:sch 1
  SubCQCInd1 { Al() -> QC-alphabet, Pro[set] } :
  for S being Element of CQC-Sub-WFF(Al())  holds Pro[S]
provided
 for S,S9 being Element of CQC-Sub-WFF(Al()),
x being bound_QC-variable of Al(),
SQ being second_Q_comp of [S,x],
k being Nat,
ll being CQC-variable_list of k, Al(),
P being (QC-pred_symbol of k,Al()),
e being Element of vSUB(Al())
holds Pro[Sub_P(P,ll,e)] & (S is Al()-Sub_VERUM implies Pro[S]) &
(Pro[S] implies Pro[Sub_not S]) &
(S`2 = (S9)`2 & Pro[S] & Pro[S9] implies Pro[CQCSub_&(S,S9)]) &
([S,x] is quantifiable & Pro[S] implies Pro[CQCSub_All([S,x], SQ)]);

:: Substitution Lemma (Ebb et al, Chapter III, 8.3)

theorem :: SUBLEMMA:89
  for S, v holds (J,v |= CQC_Sub(S) iff J,v.Val_S(v,S) |= S);