+(* Basic properties *********************************************************)
+
+(* Note: cpr_flat: does not hold in basic_1 *)
+(* Basic_1: includes: pr2_thin_dx *)
+lemma cpr_flat: ∀h,I,G,L,V1,V2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 →
+ ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡[h] ⓕ{I}V2.T2.
+#h * /2 width=1 by cpm_cast, cpm_appl/
+qed.
+
+(* Basic_1: was: pr2_head_1 *)
+lemma cpr_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 →
+ ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡[h] ②{I}V2.T.
+#h * /2 width=1 by cpm_bind, cpr_flat/
+qed.
+