-
-nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n.
-//; nqed.
-
-nlemma subst_rel: ∀A.subst A (Rel O) = A.
-nnormalize; //; nqed.
-
-nlemma subst_rel1: ∀A.∀k,i. i < k →
- subst_aux (Rel i) k A = Rel i.
-#A; #k; #i; nnormalize; #ltik;
-nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
-
-nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A k.
-#A; #k; nnormalize;
-nrewrite > (lt_to_leb_false (S k) k ?); //;
-nrewrite > (eq_to_eqb_true … (refl …)); //;
-nqed.
-
-nlemma subst_rel3: ∀A.∀k,i. k < i →
- subst_aux (Rel i) k A = Rel (i-1).
-#A; #k; #i; nnormalize; #ltik;
-nrewrite > (lt_to_leb_false (S i) k ?); /2/;
-nrewrite > (not_eq_to_eqb_false i k ?); //;
-napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
-nqed.
-
-(* versione con plus
-nlemma lift_subst_aux_k: ∀A,B.∀j,k.
- lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (j+k+1) A.
-#A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
- ##[nelim (leb (S n) k);
- ##[nrewrite > (subst_rel1 A (j+k+1) n ?);/2/;
- ##|nrewrite > (subst_rel1 A (j+k+1) (n+1) ?);/2/;
- ##]
- ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk;
- ##[nrewrite > (lt_to_leb_false (S n) k ?);
- ##[ncut (j+k+1 = n+1);##[//;##] #Heq;
- nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
- napplyS lift_lift_aux2 (* bello *);//;
- ##|/2/;
- ##]
- ##|ncut (j + k < n);
- ##[napply not_eq_to_le_to_lt;
- ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
- ##|#ltjkn;
- ncut (O < n); ##[/2/; ##] #posn;
- ncut (k ≤ n); ##[/2/; ##] #lekn;
- nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
- ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
- nrewrite > (subst_rel3 A (j+k+1) (n+1) ?);
- ##[nrewrite < (plus_minus_m_m … posn);//;
- ##|napplyS monotonic_lt_plus_l; //;
- ##]
- ##|napply le_S_S;
- napply (not_eq_to_le_to_le_minus … lekn);
- /2/; (* come fa? *)
- ##]
- ##]
- ##]
-nqed. *)
-
-naxiom lift_subst_aux_kij: ∀A,B.∀i,j,k.
- lift_aux (subst_aux B (j+k) A) k i = subst_aux (lift_aux B k i) (j+k+i) A.
-
-nlemma lift_subst_aux_k: ∀A,B.∀j,k.
- lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (S(j+k)) A.
-#A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
- ##[nelim (leb (S n) k);
- ##[nrewrite > (subst_rel1 A (S(j+k)) n ?);/2/;
- ##|nrewrite > (subst_rel1 A (S(j+k)) (n+1) ?);/2/;
- ##]
- ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk;
- ##[nrewrite > (lt_to_leb_false (S n) k ?);
- ##[ncut (S(j+k) = n+1);##[//;##] #Heq;
- nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
- napplyS lift_lift_aux2 (* bello *);//;
- ##|/2/;
- ##]
- ##|ncut (j + k < n);
- ##[napply not_eq_to_le_to_lt;
- ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
- ##|#ltjkn;
- ncut (O < n); ##[/2/; ##] #posn;
- ncut (k ≤ n); ##[/2/; ##] #lekn;
- nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
- ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
- nrewrite > (subst_rel3 A (S(j+k)) (n+1) ?);
- ##[nrewrite < (plus_minus_m_m … posn);//;
- ##|ncut (S n = n +1); /2/;
- ##]
- ##|napply le_S_S; (* /3/;*)
- napply (not_eq_to_le_to_le_minus … lekn);
- /3/; (* come fa? *)
- ##]
- ##]
- ##]
-nqed.
-
-(*
-nlemma lift_subst_aux_k: ∀A,B.∀k.
- lift_aux (subst_aux B k A) k 1 = subst_aux (lift_aux B k 1) (k+1) A.
-#A; #B; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) k); nnormalize; #Hnk;
- ##[nrewrite > (le_to_leb_true ?? Hnk);
- nrewrite > (le_to_leb_true (S n) (k +1) ?);nnormalize;/2/;
- ##|nrewrite > (lt_to_leb_false (S (n + 1)) (k+1) ?);
- ##[##2: napply le_S_S; napply (monotonic_le_plus_l 1 k n);
- napply not_lt_to_le; napply Hnk; ##]
- napply (eqb_elim n k);#eqnk;
- ##[nrewrite > (eq_to_eqb_true (n+1) (k+1) ?);/2/;
- nnormalize; nrewrite < eqnk; //; (* strano *)
- ##|nrewrite > (not_eq_to_eqb_false (n+1) (k+1) ?);/2/;
- nnormalize;
- ncut (O < n);
- ##[napply not_le_to_lt;#len;
- napply eqnk; napply le_to_le_to_eq;
- ##[napply transitive_le; //;
- ##|napply not_lt_to_le; /2/;
- ##]
- ##|#posn;
- nrewrite > (lt_to_leb_false (S (n - 1)) k ?);
- ##[nnormalize;
- (* nrewrite < (minus_plus_m_m n 1); *)
- nrewrite < (plus_minus_m_m n 1 ?);//;
- ##|napply le_S_S; napply not_eq_to_le_to_le_minus;
- ##[/2/;
- ##|napply (not_lt_to_le … Hnk);
- ##]
- ##]
- ##]
- ##]
- ##]
-nqed.