proposition: Lemma TI_intersection_equiv k : relation_equivalence (TI k) (intersection k).
proof: Proof. induction k. - intros x y. red. split. intros []. exact I. intros. exact I. - intros [x rx] [y ry]. simpl. split. + unfold TI. intros Hg. pose proof Hg. rewrite -> graph_relation_spec in H. intros. pose (H fz). simpl in y0. intuition. assert (graph_relation (TI_graph k) rx ry). rewrite graph_relation_spec. intros. clear y0. specialize (H (fs f)). simpl in H. unfold TI_graph. destruct k. depelim f. auto. do 2 red in IHk. simpl in IHk. rewrite <- IHk. apply H0. + intros [Hle Hi]. unfold TI. rewrite graph_relation_spec. intros. depelim f. simpl. auto. simpl. do 2 red in IHk. simpl in IHk. rewrite <- IHk in Hi. red in Hi. rewrite -> graph_relation_spec in Hi. clear -Hi. induction k. depelim f. specialize (Hi f). simpl in Hi. auto. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect