(* 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-.
-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/