fact: Fixpoint itree_similar_upto (i:nat) (m1 m2: itree) := match i with | O => True | S i' => match m1,m2 with | itree_leaf n1, itree_leaf n2 => n1 = n2 | itree_node t11 t12, itree_node t21 t22 => itree_similar_upto i' t11 t21 /\ itree_similar_upto i' t12 t22 | _, _ => False end end.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat