(* Forward lemmas involving same top term constructor ***********************)
+lemma cprs_fwd_cnf: ∀L,T. L ⊢ 𝐍⦃T⦄ → ∀U. L ⊢ T ➡* U → T ≃ U.
+#L #T #HT #U #H
+>(cprs_inv_cnf1 … H HT) -L -T //
+qed-.
+
(* Basic_1: was: pr3_iso_beta *)
lemma cprs_fwd_beta: ∀L,V,W,T,U. L ⊢ ⓐV. ⓛW. T ➡* U →
ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⓓV. T ➡* U.
]
qed-.
+(* Note: probably this is an inversion lemma *)
+lemma cprs_fwd_delta: ∀L,K,V1,i. ⇩[0, i] L ≡ K. ⓓV1 →
+ ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+ ∀U. L ⊢ #i ➡* U →
+ #i ≃ U ∨ L ⊢ V2 ➡* U.
+#L #K #V1 #i #HLK #V2 #HV12 #U #H
+elim (cprs_inv_lref1 … H) -H /2 width=1/
+* #K0 #V0 #U0 #HLK0 #HVU0 #HU0 #_
+lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/
+qed-.
+
lemma cprs_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡* U →
∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨
L ⊢ ⓓV. ⓐV2. T ➡* U.
]
qed-.
-lemma cprs_fwd_tau: â\88\80L,W,T,U. L â\8a¢ â\93£W. T ➡* U →
- â\93£W. T ≃ U ∨ L ⊢ T ➡* U.
+lemma cprs_fwd_tau: â\88\80L,W,T,U. L â\8a¢ â\93\9dW. T ➡* U →
+ â\93\9dW. T ≃ U ∨ L ⊢ T ➡* U.
#L #W #T #U #H
elim (cprs_inv_cast1 … H) -H /2 width=1/ *
#W0 #T0 #_ #_ #H destruct /2 width=1/