#H elim (Ht H)
qed.
-(* Basic inversions *********************************************************)
+(* Basic destructions *******************************************************)
-lemma in_ppc_comp_trans (t) (p):
+lemma in_comp_tpc_trans (t) (p):
p ϵ t → t ϵ 𝐏 → p ϵ 𝐏.
#t #p #Hp #Ht
@(Ht … Hp)
qed-.
-lemma tpc_e (t): 𝐞 ϵ t → t ϵ 𝐏 → ⊥.
-/2 width=5 by in_ppc_comp_trans/ qed-.
+(* Basic inversions *********************************************************)
+
+lemma tpc_inv_empty (t):
+ (𝐞) ϵ t → t ϵ 𝐏 → ⊥.
+/2 width=5 by in_comp_tpc_trans/ qed-.