proposition: Lemma Funext_downward_closed@{i j max i' j' max' | i <= max, j <= max, i' <= max', j' <= max', i' <= i, j' <= j} `{H : Funext_type@{i j max}} : Funext_type@{i' j' max'}.
proof: Proof. hnf in *. exact (fun A P => H A P). Defined.
imports: HoTT.Basics HoTT.Types Metatheory.Core