| (Arrow T1 T2) \Rightarrow (Arrow (subst_type_nat T1 U i) (subst_type_nat T2 U i))
| (Forall T1 T2) \Rightarrow (Forall (subst_type_nat T1 U i) (subst_type_nat T2 U (S i))) ].
-(*** height of T's syntactic tree ***)
-
-let rec t_len T \def
- match T with
- [(TVar n) \Rightarrow (S O)
- |(TFree X) \Rightarrow (S O)
- |Top \Rightarrow (S O)
- |(Arrow T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))
- |(Forall T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))].
-
(*** definitions about lists ***)
definition fv_env : (list bound) \to (list nat) \def
interpretation "subst bound var" 'substvar S T n =
(cic:/matita/Fsub/defn/subst_type_nat.con S T n).
-notation "hvbox(|T|)"
- non associative with precedence 30 for @{ 'tlen $T }.
-interpretation "type length" 'tlen T =
- (cic:/matita/Fsub/defn/t_len.con T).
-
notation "hvbox(!X ⊴ T)"
non associative with precedence 60 for @{ 'subtypebound $X $T }.
interpretation "subtyping bound" 'subtypebound X T =
|destruct H5|*:destruct H6]
qed.
+(*
(* elim vs inversion *)
lemma JS_trans_TFree: ∀G,T,X.G ⊢ T ⊴ (TFree X) →
∀U.G ⊢ (TFree X) ⊴ U → G ⊢ T ⊴ U.
|apply (SA_Trans_TVar ? ? ? ? H1);apply (H3 Y);assumption
|*:destruct H5]]
qed.
+*)
lemma fv_append : ∀G,H.fv_env (G @ H) = (fv_env G @ fv_env H).
intro;elim G;simplify;autobatch paramodulation;
-qed.
\ No newline at end of file
+qed.