proposition: Lemma itree_similar_eq : itree_similar = similar itree_family.
proof: Proof. Proof using. extens. intros t1 t2. iff H. intros i. hnf. gen t1 t2. induction i; simpl; introv H. auto. inversions~ H. hnf in H. gen t1 t2. cofix IH. intros t1 t2. destruct t1; destruct t2; introv H; lets H1: (H 1); simpl in H1; inverts H1; constructor. apply IH. intros i. lets_simpl HSi: (H (S i)). autos*. apply IH. intros i. lets_simpl HSi: (H (S i)). autos*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat TLC.LibNat