proposition: Lemma swap_appR_eq : forall E PtL PtR A B (Ml: E |- PtL := A --> B) (Mr: E |- PtR := A) (pos: Pos (buildT Ml)) (Mpos: PlaceHolder (PAppL Mr pos)) (Npos: PlaceHolder (PAppL Mr pos)) (Lapp: isApp (swap Mpos)) (Rapp: isApp (swap Npos)), appBodyR Lapp = appBodyR Rapp.
proof: Proof. intros E PtL PtR A B Ml Mr pos Mpos Npos Lapp Rapp. apply term_eq. do 2 rewrite appBodyR_env. do 2 rewrite swap_env_eq. trivial. assert (tL: term (swap Mpos) = swap_term pos (proj1_sig2 Mpos) @@ PtR). rewrite swap_term_is; try_solve. assert (tR: term (swap Npos) = swap_term pos (proj1_sig2 Npos) @@ PtR). rewrite swap_term_is; try_solve. rewrite (appBodyR_term (swap Mpos) tL). rewrite (appBodyR_term (swap Npos) tR). trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)