proposition: Lemma function_subrelationA ls c (H : is_finite_forA ls c) : forall x y : C, RT_closure (fun x0 y0 : C => function_relationA (F x0) (F y0)) y c -> function_relationA (F x) (F y) -> (fun x0 y0 : C => iterated_prod_relationA_of eqA R (fun _ : B -> A => length ls) (iterated_prod_of_function_for ls) (F x0) (F y0)) x y.
proof: Proof. intros g h Hhf Hgh; cbv beta. assert (Hfinh : is_finite_forA ls h) by (rewrite Hhf; assumption). assert (Hfing : is_finite_forA ls g) by (unfold is_finite_forA; rewrite Hgh; assumption). unfold iterated_prod_relationA_of, function_relationA, iterated_prod_of_function_for in *. rewrite nat_eq_transfer_refl. destruct Hgh as [Hle Hne]. destruct Hne as [b Hne]. assert (Hin : ~~SetoidList.InA eqv b ls). { intro Hnin. rewrite Hfinh in Hne by assumption. eauto with nocore. } rewrite SetoidList.InA_alt in Hin. move ls at bottom. clear H Hfinh Hfing. induction ls as [|x xs IHxs]; [ | destruct (Hle x) as [Heqx|Hlex]; [ right; split; [ | apply IHxs; clear IHxs ] | left ] ]; simpl; unfold prod_relationA; simpl in *; repeat match goal with | _ => congruence | _ => tauto | [ H : ex _ |- _ ] => destruct H | [ H : and _ _ |- _ ] => destruct H | [ H : or _ _ |- _ ] => destruct H | _ => progress subst | _ => progress eauto | _ => solve [ exfalso; eauto ] | [ H : ~~(exists x, _ /\ False) |- _ ] => exfalso; apply H; clear | _ => intro | [ |- and _ _ ] => split | [ H : ~~_ |- False ] => apply H; clear H end. Qed.
imports: Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf Coq.Lists.SetoidList Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat