(**************************************************************************)
include "basic_2/reducibility/cnf.ma".
+include "basic_2/computation/tprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
@(cprs_strap1 … IHT2) -IHT2 /2 width=1/
qed.
+(* Basic_1: was: pr3_pr1 *)
+lemma tprs_cprs: ∀T1,T2. T1 ➡* T2 → ∀L. L ⊢ T1 ➡* T2.
+#T1 #T2 #H @(tprs_ind … H) -T2 /2 width=1/ /3 width=3/
+qed.
+
(* Basic inversion lemmas ***************************************************)
(* Basic_1: was: pr3_gen_sort *)
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
qed-.
+lemma tprs_inv_cnf1: ∀T,U. T ➡* U → ⋆ ⊢ 𝐍⦃T⦄ → T = U.
+/3 width=3 by tprs_cprs, cprs_inv_cnf1/ qed-.
+
(* Basic_1: removed theorems 10:
clear_pr3_trans pr3_cflat pr3_gen_bind
pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12