proposition: Lemma open_rec_lc_core_automated : forall e j v i u, i <> j -> {j ~> v} e = {i ~> u} ({j ~> v} e) -> e = {i ~> u} e.
proof: Proof. Proof with try solve [eauto | congruence]. induction e; intros j v i u Neq H; simpl in *; try solve [inversion H; f_equal; eauto]. Case "bvar". destruct (j == n)... destruct (i == n)... Qed.
imports: Metalib.Metatheory String