proposition: Lemma itree_similar_upto_equiv : forall i, equiv (itree_similar_upto i).
proof: Proof. Proof using. constructor; unfolds. induction i; intros; simple~. destruct~ x. induction i; intros; simple~. destruct x; destruct y; simpls*. induction i; intros; simple~. destruct x; destruct y; destruct z; simpls*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat