proposition: Lemma size_change_wf {k} (n : nat) (T : fin n -> relation (k_tuple_type k)) (graphs : list (graph k)) (approx : approximates_family graphs (fin_union T)) (S : list (graph k)) (Strans : is_transitive_closure graphs S) (R : relation (k_tuple_type k)) (AF : AlmostFull R) : (forall G, In G S -> forall x y, graph_relation G x y /\ R y x -> False) -> well_founded (fin_union T).
proof: Proof. intros H. apply (af_wf _ R). intros x y [Txy Ryx]. rewrite <- clos_trans_t1n_iff in Txy. apply clos_trans_power in Txy as [k' Tkxy]. red in Strans. destruct (in_transitive_closure graphs S (fin_union T) approx Strans k') as [g' [Ings Hg]]. apply Hg in Tkxy. clear Hg. induction g'; simpl in Tkxy. elim Tkxy. destruct Tkxy. specialize (Ings a). forward Ings by constructor; auto. now apply (H a Ings x y). apply IHg'; auto. intros. apply Ings; intuition. Defined.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect