proposition: Lemma appBodyL_swap_in_appR : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A) (pos: Pos (buildT Mr)) (Mpos: PlaceHolder pos) (MLpos: PlaceHolder (PAppR Ml pos)) (MLapp: isApp (swap MLpos)), proj1_sig2 Mpos = proj1_sig2 MLpos -> appBodyL (M := swap MLpos) MLapp = buildT Ml.
proof: Proof. intros. apply term_eq. rewrite appBodyL_env. rewrite swap_env_eq; trivial. rewrite (@appBodyL_term (swap MLpos) PtL (swap_term pos (proj1_sig2 MLpos))); trivial. rewrite swap_term_is; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)