Lemma filterim_htrue : isfilter_htrue filterim. Proof. apply Htrue. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.