proposition: Lemma size_change_wf_fam {k} (n : nat) (T : fin n -> relation (k_tuple_type k)) (graphs : fin n -> graph k) (approx : forall f, approximates (graphs f) (T f)) (S : list (graph k)) (Strans : is_transitive_closure (fin_list 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. assert(approximates_family (fin_list graphs) (fin_union T)). { clear -approx. induction n. simpl. red. auto. red. simpl. auto. red. intros x y Rxy. specialize (IHn (fun f => T (fs f)) (fun f => graphs (fs f)) (fun f => approx (fs f))). do 2 red in IHn. specialize (IHn x y). destruct Rxy. simp fin_list. simpl. left. now apply approx. intuition. simp fin_list. simpl. intuition. } destruct (in_transitive_closure (fin_list graphs) S (fin_union T) H0 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