proposition: Lemma swap_in_abs : forall E Pt A B (M: E |- \A => Pt := A --> B) (Min: decl A E |- Pt := B) (pos: Pos (buildT Min)) (Mpos: PlaceHolder pos) (Min_pos: PlaceHolder (PAbs pos)) (Min_abs: isAbs (swap Min_pos)), proj1_sig2 Mpos = proj1_sig2 Min_pos -> swap Mpos = absBody (M := swap Min_pos) Min_abs.
proof: Proof. intros E Pt A B M Min pos Mpos Min_pos Min_abs M_MN. apply term_eq. rewrite absBody_env. do 2 rewrite swap_env_eq; try_solve. rewrite abs_type with (A:=A) (B:=B); trivial. rewrite swap_type_eq; trivial. rewrite swap_term_is. rewrite absBody_term with (A:=A) (Pt:=swap_term pos (proj1_sig2 Mpos)); trivial. rewrite swap_term_is; try_solve. Qed.
imports: CoLoR(RelExtras ListExtras TermsBuilding)