proposition: Lemma placeHolder_appR : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A) (pos: Pos (buildT Mr)) (N: PlaceHolder (PAppR Ml pos)), { W: PlaceHolder pos | proj1_sig2 W = proj1_sig2 N }.
proof: Proof. intros E PtL PtR A B Ml Mr pos N. exists N; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)