proposition: Lemma compose_approximates {k} (G0 G1 : graph k) (R0 R1 : relation (k_tuple_type k)) : approximates G0 R0 -> approximates G1 R1 -> approximates (G0 ⋅ G1) (compose_rel R0 R1).
proof: Proof. unfold approximates. intros ag0 ag1. intros x z [y [Hxy Hyz]]. rewrite graph_relation_spec. intros f. specialize (ag0 _ _ Hxy). specialize (ag1 _ _ Hyz). rewrite -> graph_relation_spec in ag0, ag1. specialize (ag0 f). funelim (graph_compose G0 G1 f). now rewrite Heq in ag0. rewrite Heq0 in ag0. specialize (ag1 arg1). rewrite Heq in ag1. destruct weight, weight'; simpl; try lia. specialize (ag1 arg1). now rewrite Heq in ag1. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect