(* *)
(**************************************************************************)
+include "delayed_updating/syntax/prototerm.ma".
include "delayed_updating/syntax/path_proper.ma".
include "ground/lib/subset_ext_equivalence.ma".
interpretation
"proper condition (prototerm)"
- 'PredicatePTail t = (subset_ext_p1 path ppc t).
+ 'ClassP = (subset_ext_p1 path ppc).
(* Basic constructions ******************************************************)
lemma tpc_i (t):
- (π β§ΈΟ΅ t) β κt.
+ (π β§ΈΟ΅ t) β t Ο΅ π.
#t #Ht * //
#H elim (Ht H)
qed.
+(* Basic destructions *******************************************************)
+
+lemma in_comp_tpc_trans (t) (p):
+ p Ο΅ t β t Ο΅ π β p Ο΅ π.
+#t #p #Hp #Ht
+@(Ht β¦ Hp)
+qed-.
+
(* Basic inversions *********************************************************)
-lemma tpc_e (t): κt β π Ο΅ t β β₯.
-/2 width=5 by subset_in_inv_ext_p1_dx/ qed-.
+lemma tpc_inv_empty (t):
+ (π) Ο΅ t β t Ο΅ π β β₯.
+/2 width=5 by in_comp_tpc_trans/ qed-.