[PVS-Help] Discharging TCC

["Anup Bhattacharjee" <anup.bhattacharjee@xxxxxxxxx>]

Can you help me to understand how to discharge the tcc in this theory
list_props[T: TYPE]: THEORY
BEGIN
    importing list_adt
    l,l1,l2: VAR list[T]
    cons_l: VAR (cons?[T])
    a,b,c: VAR T
    P: VAR [list[T] -> bool]
    add(l,a): (cons?[T]) = append(l, cons(a, null))
    length_add: LEMMA length(add(l,a)) = length(l) + 1
    length_non_zero: LEMMA length(l) = 0 IFF l = null
    cons_to_add: LEMMA FORALL cons_l: EXISTS a, l: cons_l=add(l,a)
     add_induction:PROPOSITION P(null) AND (FORALL l,a: P(l) IMPLIES P(add(l,a))) IMPLIES (FORALL l: P(l))
END list_props

Thanks in advance.
Anup