tpr V1 V2 โ tpr T1 T2 โ โ. ๐{I} V2 โข T2 [0, 1] โซ T โ
tpr (๐{I} V1. T1) (๐{I} V2. T)
| tpr_theta: โV,V1,V2,W1,W2,T1,T2.
- tpr V1 V2 รข\86\92 รข\86\91[0,1] V2 รข\89ยก V รข\86\92 tpr W1 W2 รข\86\92 tpr T1 T2 รข\86\92
+ tpr V1 V2 รข\86\92 รข\87\91[0,1] V2 รข\89ยก V รข\86\92 tpr W1 W2 รข\86\92 tpr T1 T2 รข\86\92
tpr (๐{Appl} V1. ๐{Abbr} W1. T1) (๐{Abbr} W2. ๐{Appl} V. T2)
-| tpr_zeta : รข\88\80V,T,T1,T2. รข\86\91[0,1] T1 รข\89ยก T รข\86\92 tpr T1 T2 รข\86\92
+| tpr_zeta : รข\88\80V,T,T1,T2. รข\87\91[0,1] T1 รข\89ยก T รข\86\92 tpr T1 T2 รข\86\92
tpr (๐{Abbr} V. T) T2
| tpr_tau : โV,T1,T2. tpr T1 T2 โ tpr (๐{Cast} V. T1) T2
.
(* Basic properties *********************************************************)
lemma tpr_bind: โI,V1,V2,T1,T2. V1 โ V2 โ T1 โ T2 โ
- ๐{I} V1. T1 โ ๐{I} V2. T2.
-/2/ qed.
+ ๐{I} V1. T1 โ ๐{I} V2. T2.
+/2 width=3/ qed.
(* Basic_1: was by definition: pr0_refl *)
lemma tpr_refl: โT. T โ T.
#T elim T -T //
-#I elim I -I /2/
+#I elim I -I /2 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
fact tpr_inv_atom1_aux: โU1,U2. U1 โ U2 โ โI. U1 = ๐{I} โ U2 = ๐{I}.
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
[ //
| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
(* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
lemma tpr_inv_atom1: โI,U2. ๐{I} โ U2 โ U2 = ๐{I}.
-/2/ qed.
+/2 width=3/ qed-.
fact tpr_inv_bind1_aux: โU1,U2. U1 โ U2 โ โI,V1,T1. U1 = ๐{I} V1. T1 โ
(โโV2,T2,T. V1 โ V2 & T1 โ T2 &
โ. ๐{I} V2 โข T2 [0, 1] โซ T &
U2 = ๐{I} V2. T
) โจ
- รข\88\83รข\88\83T. รข\86\91[0,1] T รข\89ยก T1 & T รข\87\92 U2 & I = Abbr.
-#U1 #U2 * -U1 U2
+ รข\88\83รข\88\83T. รข\87\91[0,1] T รข\89ยก T1 & T รข\87\92 U2 & I = Abbr.
+#U1 #U2 * -U1 -U2
[ #J #I #V #T #H destruct
| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
-| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/
+| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/
+| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct /3 width=3/
| #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
]
qed.
โ. ๐{I} V2 โข T2 [0, 1] โซ T &
U2 = ๐{I} V2. T
) โจ
- รข\88\83รข\88\83T. รข\86\91[0,1] T รข\89ยก T1 & T รข\87\92 U2 & I = Abbr.
-/2/ qed.
+ รข\88\83รข\88\83T. รข\87\91[0,1] T รข\89ยก T1 & T รข\87\92 U2 & I = Abbr.
+/2 width=3/ qed-.
(* Basic_1: was pr0_gen_abbr *)
lemma tpr_inv_abbr1: โV1,T1,U2. ๐{Abbr} V1. T1 โ U2 โ
โ. ๐{Abbr} V2 โข T2 [0, 1] โซ T &
U2 = ๐{Abbr} V2. T
) โจ
- รข\88\83รข\88\83T. รข\86\91[0,1] T รข\89ยก T1 & T รข\87\92 U2.
+ รข\88\83รข\88\83T. รข\87\91[0,1] T รข\89ยก T1 & T รข\87\92 U2.
#V1 #T1 #U2 #H
elim (tpr_inv_bind1 โฆ H) -H * /3 width=7/
-qed.
+qed-.
fact tpr_inv_flat1_aux: โU1,U2. U1 โ U2 โ โI,V1,U0. U1 = ๐{I} V1. U0 โ
โจโจ โโV2,T2. V1 โ V2 & U0 โ T2 &
U0 = ๐{Abst} W. T1 &
U2 = ๐{Abbr} V2. T2 & I = Appl
| โโV2,V,W1,W2,T1,T2. V1 โ V2 & W1 โ W2 & T1 โ T2 &
- รข\86\91[0,1] V2 รข\89ยก V &
+ รข\87\91[0,1] V2 รข\89ยก V &
U0 = ๐{Abbr} W1. T1 &
U2 = ๐{Abbr} W2. ๐{Appl} V. T2 &
I = Appl
| (U0 โ U2 โง I = Cast).
-#U1 #U2 * -U1 U2
+#U1 #U2 * -U1 -U2
[ #I #J #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/
+| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
+| #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=8/
| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H
- destruct -J V1 T0 /3 width=12/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=12/
| #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
-| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/
+| #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
]
qed.
U0 = ๐{Abst} W. T1 &
U2 = ๐{Abbr} V2. T2 & I = Appl
| โโV2,V,W1,W2,T1,T2. V1 โ V2 & W1 โ W2 & T1 โ T2 &
- รข\86\91[0,1] V2 รข\89ยก V &
+ รข\87\91[0,1] V2 รข\89ยก V &
U0 = ๐{Abbr} W1. T1 &
U2 = ๐{Abbr} W2. ๐{Appl} V. T2 &
I = Appl
| (U0 โ U2 โง I = Cast).
-/2/ qed.
+/2 width=3/ qed-.
(* Basic_1: was pr0_gen_appl *)
lemma tpr_inv_appl1: โV1,U0,U2. ๐{Appl} V1. U0 โ U2 โ
U0 = ๐{Abst} W. T1 &
U2 = ๐{Abbr} V2. T2
| โโV2,V,W1,W2,T1,T2. V1 โ V2 & W1 โ W2 & T1 โ T2 &
- รข\86\91[0,1] V2 รข\89ยก V &
+ รข\87\91[0,1] V2 รข\89ยก V &
U0 = ๐{Abbr} W1. T1 &
U2 = ๐{Abbr} W2. ๐{Appl} V. T2.
#V1 #U0 #U2 #H
elim (tpr_inv_flat1 โฆ H) -H * /3 width=12/ #_ #H destruct
-qed.
+qed-.
+
+(* Note: the main property of simple terms *)
+lemma tpr_inv_appl1_simple: โV1,T1,U. ๐{Appl} V1. T1 โ U โ ๐[T1] โ
+ โโV2,T2. V1 โ V2 & T1 โ T2 &
+ U = ๐{Appl} V2. T2.
+#V1 #T1 #U #H #HT1
+elim (tpr_inv_appl1 โฆ H) -H *
+[ /2 width=5/
+| #V2 #W #W1 #W2 #_ #_ #H #_ destruct
+ elim (simple_inv_bind โฆ HT1)
+| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
+ elim (simple_inv_bind โฆ HT1)
+]
+qed-.
(* Basic_1: was: pr0_gen_cast *)
lemma tpr_inv_cast1: โV1,T1,U2. ๐{Cast} V1. T1 โ U2 โ
[ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
| #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
]
-qed.
+qed-.
fact tpr_inv_lref2_aux: โT1,T2. T1 โ T2 โ โi. T2 = #i โ
โจโจ T1 = #i
- | รข\88\83รข\88\83V,T,T0. รข\86\91[O,1] T0 รข\89ยก T & T0 รข\87\92 #i &
+ | รข\88\83รข\88\83V,T,T0. รข\87\91[O,1] T0 รข\89ยก T & T0 รข\87\92 #i &
T1 = ๐{Abbr} V. T
| โโV,T. T โ #i & T1 = ๐{Cast} V. T.
-#T1 #T2 * -T1 T2
-[ #I #i #H destruct /2/
+#T1 #T2 * -T1 -T2
+[ #I #i #H destruct /2 width=1/
| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
| #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
| #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
-| #V #T1 #T2 #HT12 #i #H destruct /3/
+| #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
]
qed.
lemma tpr_inv_lref2: โT1,i. T1 โ #i โ
โจโจ T1 = #i
- | รข\88\83รข\88\83V,T,T0. รข\86\91[O,1] T0 รข\89ยก T & T0 รข\87\92 #i &
+ | รข\88\83รข\88\83V,T,T0. รข\87\91[O,1] T0 รข\89ยก T & T0 รข\87\92 #i &
T1 = ๐{Abbr} V. T
| โโV,T. T โ #i & T1 = ๐{Cast} V. T.
-/2/ qed.
+/2 width=3/ qed-.
(* Basic_1: removed theorems 3:
pr0_subst0_back pr0_subst0_fwd pr0_subst0