``` ```

``` Require Import Calculus. Module SetProgram(My_Program: Program). Import My_Program. Require Proofs_Subclassing. Module My_Proofs_Subclassing := Proofs_Subclassing.SetProgram(My_Program). Import My_Proofs_Subclassing. Import My_Proofs_TypeOrdering. Import My_Proofs_Miscellaneous. Import My_WellFormedness. Import My_Semantics. Import My_Typing. Import My_TypeOrdering. Import My_DeBruijn. Import My_Substitutions. Import My_Subclassing. Definition lemmaA23_prop1 (G: Env) (p: Path) (T: type) (H: (PathTyping G p T)): Prop :=   (Gen_PathTyping G p T) . Definition lemmaA23_prop2 (G: Env) (T: type) (U: type) (H: (Subtyping G T U)): Prop :=   (Gen_Subtyping G T U) . Definition lemmaA23_prop3 (G: Env) (C: ClassSym) (fvs: FieldValueList) (H: (FieldValueListTyping G C fvs)): Prop :=   (Gen_FieldValueListTyping G C fvs) . ```
 Unstructuring derivations
``` Lemma lemmaA23_2:   forall (G: Env) (T: type) (U: type),     (Subtyping G T U) ->     (Gen_Subtyping G T U) . ```
 Unstructuring derivations
``` Lemma lemmaA23_1:   forall (G: Env) (p: Path) (T: type),     (PathTyping G p T) ->     (Gen_PathTyping G p T) . Definition lemmaA24_prop_1 (G: Env) (TA T: type) (H: (Subtyping G TA T)): Prop :=   forall (C A: ClassSym),     G = (classEnv C) ->     TA = (type_class A) ->     ~(this_in_type T) ->     (Subtyping rootEnv (type_class A) T) . Definition lemmaA24_prop_2 (G: Env) (p: Path) (T: type) (H: (PathTyping G p T)): Prop :=   forall (C: ClassSym) (v: Value),     G = (classEnv C) ->     p = (Path_value v) ->     ~(this_in_type T) ->     (PathTyping rootEnv (Path_value v) T) . Definition lemmaA24_prop_3 (G: Env) (B: ClassSym) (fvs: FieldValueList) (H: (FieldValueListTyping G B fvs)): Prop :=   forall (C: ClassSym),     G = (classEnv C) ->     (FieldValueListTyping rootEnv B fvs) . ```
 Strengthening - 2
``` Lemma lemmaA24_2_aux:   forall (G: Env) (p: Path) (T: type) (H: PathTyping G p T),     (lemmaA24_prop_2 G p T H) . ```
 Strengthening - 2
``` Lemma lemmaA24_2:   forall (C: ClassSym) (v: Value) (T: type),     (PathTyping (classEnv C) (Path_value v) T) ->     ~(this_in_type T) ->     (PathTyping rootEnv (Path_value v) T) . ```
 Admissibility of transitivity for class type subtyping
``` Lemma lemmaA25:   forall (G G' G'': Env) (A B C: ClassSym),     (Subtyping G (type_class A) (type_class B)) ->     (Subtyping G' (type_class B) (type_class C)) ->     (Subtyping G'' (type_class A) (type_class C)) . ```
 Substitution for self in structured derivations - 1
``` Definition lemmaA26_prop_1 (G: Env) (p: Path) (T: type) (H: (PathTyping G p T)): Prop :=   forall (v: Value) (C A: ClassSym),     (PathTyping rootEnv (Path_value v) (type_class C)) ->     G = (classEnv C) ->     T = (type_class A) ->     (PathTyping rootEnv (thisSubst_in_path p (Path_value v)) (type_class A)) . ```
 Substitution for self in structured derivations - 2
``` Definition lemmaA26_prop_2 (G: Env) (T U: type) (H: (Subtyping G T U)): Prop :=   forall (v: Value) (C: ClassSym),     (PathTyping rootEnv (Path_value v) (type_class C)) ->     G = (classEnv C) ->     (Subtyping rootEnv (thisSubst_in_type T (Path_value v)) (thisSubst_in_type U (Path_value v))) . ```
 Substitution for self in structured derivations - 1
``` Lemma lemmaA26_1_aux:   forall (G: Env) (p: Path) (T: type) (H: (PathTyping G p T)),     (lemmaA26_prop_1 G p T H). ```
 Substitution for self in structured derivations - 1
``` Lemma lemmaA26_1:   forall (v: Value) (C: ClassSym),     (PathTyping rootEnv (Path_value v) (type_class C)) ->     forall (A: ClassSym) (p: Path),       (PathTyping (classEnv C) p (type_class A)) ->       (PathTyping rootEnv (thisSubst_in_path p (Path_value v)) (type_class A)) . ```
 Substitution for self in structured derivations - 2
``` Lemma lemmaA26_2_aux:   forall (G: Env) (T U: type) (H: (Subtyping G T U)),     (lemmaA26_prop_2 G T U H). ```
 Substitution for self in structured derivations - 2
``` Lemma lemmaA26_2:   forall (v: Value) (C: ClassSym) (T U: type),     (PathTyping rootEnv (Path_value v) (type_class C)) ->     (Subtyping (classEnv C) T U) ->     (Subtyping rootEnv (thisSubst_in_type T (Path_value v)) (thisSubst_in_type U (Path_value v))) . Import Type_Multiset. Import Type_MultisetOrder. Import MSet. Definition lemmaA27_prop (tm: Type_Multiset.Multiset): Prop :=   forall (T S U: type),     tm = ({{T}} + {{S}} + {{U}}) ->     (Subtyping rootEnv T S) ->     (Subtyping rootEnv S U) ->     (Subtyping rootEnv T U) . ```
 Admissibility of transitivity for structured subtyping
``` Lemma lemmaA27:   forall (T S U: type),     (Subtyping rootEnv T S) ->     (Subtyping rootEnv S U) ->     (Subtyping rootEnv T U) . Definition lemmaA28_prop1 (G: Env) (p: Path) (T: type) (H: (Gen_PathTyping G p T)): Prop :=   forall (v: Value),     (G = rootEnv) ->     (p = (Path_value v)) ->     (PathTyping rootEnv p T) . Definition lemmaA28_prop2 (G: Env) (T: type) (U: type) (H: (Gen_Subtyping G T U)): Prop :=   (G = rootEnv) ->   (Subtyping rootEnv T U) . Definition lemmaA28_prop3 (G: Env) (C: ClassSym) (fvs: FieldValueList) (H: (Gen_FieldValueListTyping G C fvs)): Prop :=   (G = rootEnv) ->   (FieldValueListTyping rootEnv C fvs) . ```
 Structuring derivations -- subtyping
``` Lemma lemmaA28_2:   forall (T: type) (U: type),     (Gen_Subtyping rootEnv T U) ->     (Subtyping rootEnv T U) . ```
 Structuring derivations -- path typing
``` Lemma lemmaA28_1:   forall (v: Value) (T: type),     (Gen_PathTyping rootEnv (Path_value v) T) ->     (PathTyping rootEnv (Path_value v) T) . End SetProgram. ```
Index