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