We want to prove the following lemma:

! n. ! t. ~ ( varoccursinterm n t  ) ==> 
      ! sys. 
       ( CARD  ( systemvarset ( applsystem ( substsingle n t  ) sys ))) <
       ( CARD  ( systemvarset ( Addequation sys ( Variable n ) t )))

We do this using pre-proved HOL theorem CARD_PSUBSET, which says that |- !a b. a PSUBSET b /\ FINITE b ==> CARD a < CARD b. Thus, we need to prove that systemvarset ( applsystem ( substsingle n t  ) sys ) is a proper subset of systemvarset ( Addequation sys ( Variable n ) t ) (we do this in the 2nd part) and that those sets are not equal (the 1st part).


PART 0

xcLemma0:
! t. ( FINITE ( termvarset t ))


xcLemma1:
! sys. ( FINITE ( systemvarset sys ))

PART I

xLemma01:
  !a t n. (\m. if n = m then t else Variable m) a =
               (if n = a then t else Variable a)

xLemma03:
!n:num t:term. n IN termvarset t <=> varoccursinterm n t

xLemma04:
!n t. !ter. (n IN termvarset (applterm (substsingle n t) ter)) ==> varoccursinterm n t

xLemma06:
!P:bool n:num A B C.
(n IN {x | x IN A \/ x IN {x | x IN B \/ x IN C}} ==> P)
       = (n IN A \/ n IN B \/ n IN C  ==> P)

xLemma07:
! n. ! t. ! sys. ( n IN systemvarset ( applsystem ( substsingle n t  ) sys ))
           ==> ( varoccursinterm n t )

xLemma08:
! n. ! t. ~(varoccursinterm n t)
        ==>  ! sys. ~(n IN systemvarset ( applsystem ( substsingle n t ) sys))

xLemma09:
! n. ! t. ~(varoccursinterm n t)
         ==> ! sys. n IN (systemvarset ( Addequation sys ( Variable n ) t ))

xLemma10:
! n. ! t. ~(varoccursinterm n t) ==>
  ~( (systemvarset ( Addequation sys ( Variable n ) t ))  = 
     (systemvarset ( applsystem ( substsingle n t ) sys)) )

PART II

xLemma11:
!n:num. !t:term. !m:num. !x:term. ~(m = n) ==> (varoccursinterm m x)
               ==> (varoccursinterm m (applterm (substsingle n t) x))

xLemma12:
!ter:term n:num t:term. ~(varoccursinterm n t) ==>
         !x:num. ~(x = n) ==> (x IN (termvarset ter))
               ==> (x IN (termvarset (applterm (substsingle n t) ter)))

xLemma13:
! n. ! t. ~ ( varoccursinterm n t  ) ==> 
      ! sys. 
       !v. (v = n) ==> v IN ( systemvarset ( applsystem ( substsingle n t  ) sys )) ==>
                       v IN ( systemvarset ( Addequation sys ( Variable n ) t ))

xLemma14:
!term v n t. varoccursinterm v (applterm (substsingle n t) term)
        ==> varoccursinterm v term \/ varoccursinterm v t

xLemma15:
!term v n t. v IN termvarset (applterm (substsingle n t) term)
        ==> v IN termvarset term \/ v IN termvarset t

xLemma16:
!v t n term. ~(v IN termvarset t) ==> v IN termvarset (applterm (substsingle n t) term)
        ==> v IN termvarset term

xLemma17:
!v n t sys.
v IN systemvarset (applsystem (substsingle n t) sys)
    ==> (v IN systemvarset sys) \/ v IN termvarset t

xLemma18:
! n. ! t. ~ ( varoccursinterm n t  ) ==> 
      ! sys. 
       !v. ~(v = n) ==> v IN ( systemvarset ( applsystem ( substsingle n t ) sys )) ==>
                        v IN ( systemvarset ( Addequation sys ( Variable n ) t ))`;;

xLemma19:
! n. ! t. ~ ( varoccursinterm n t  ) ==> 
      ! sys. 
       !v. v IN ( systemvarset ( applsystem ( substsingle n t  ) sys )) ==>
           v IN ( systemvarset ( Addequation sys ( Variable n ) t ))

xLemma20:
! n. ! t. ~ ( varoccursinterm n t  ) ==> 
      ! sys. 
       (systemvarset ( applsystem ( substsingle n t ) sys)) SUBSET
       (systemvarset ( Addequation sys ( Variable n ) t))

PART III

finalLemma:
! n. ! t. ~ ( varoccursinterm n t  ) ==> 
      ! sys. 
       ( CARD  ( systemvarset ( applsystem ( substsingle n t  ) sys ))) <
       ( CARD  ( systemvarset ( Addequation sys ( Variable n ) t )))