##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
- nnormalize;/2/; napply (not_to_not … Hnk);//;
+ nnormalize;/2/
##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
##]
##]
subst (lift B i (S k)) j A = (lift B i k).
#A; #B; nelim B; nnormalize; /2/;
##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
- napply eq_f2;/2/; napply Hind2;
+ napply eq_f2; /2/; napply Hind2;
napplyS (monotonic_le_plus_l 1);//
##|#n; #i; #j; #k; #leij; #ltjk;
napply (leb_elim (S n) i); nnormalize; #len;
##[nrewrite > eqni;
nrewrite > (le_to_leb_true i (k+i) ?); //;
nrewrite > (subst_rel2 …); nnormalize;
- napply symmetric_eq;
+ napply sym_eq;
napplyS (lift_subst_ijk C B i k O);
##|napply (leb_elim (S (n-1)) (k+i)); #nk;
##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);