proposition: Lemma closed_monotonic: forall `{Lift T}, LiftLift -> forall k t, closed k t -> forall j, j >= k -> closed j t.
proof: Proof. do 6 intro. assert (forall i, closed (i + k) t). induction i. assumption. replace (S i + k) with (1 + (i + k)) by lia. eauto using closed_increment with typeclass_instances. intros j ?. replace j with ((j - k) + k) by lia. eauto. Qed.
imports: Arith Lia Dblib.DblibTactics