proposition: Lemma subst_preserves_closed: forall `{Lift V, Lift T, Subst V T}, @LiftSubst2 V _ T _ _ -> forall k (v : V) (t : T), closed k v -> closed (S k) t -> closed k (subst v 0 t).
proof: Proof. unfold closed. intros. rewrite lift_subst_2 by lia. simpl. change (1 + k) with (S k). congruence. Qed.
imports: Arith Lia Dblib.DblibTactics