proposition: Lemma placeHolder_abs : forall E Pt A B (Mb: decl A E |- Pt := B) (pos: Pos (buildT Mb)) (N: PlaceHolder (PAbs pos)), { W: PlaceHolder pos | proj1_sig2 W = proj1_sig2 N }.
proof: Proof. intros E Pt A B Mb pos N. exists N; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)