proposition: Lemma interp_domain_ext : forall l1 l2 b, (forall k, nth 0 l1 k = nth 0 l2 k) -> interp_domain l1 b -> interp_domain l2 b.
proof: Proof. intros l1 l2 b Hl. revert l1 l2 Hl. induction b using domain_ind' ; try easy ; simpl => l1 l2 Hl. by rewrite (interp_ext _ _ _ Hl). now rewrite -(eq_map (fun e => interp_ext _ _ e Hl)). intros Hb. now rewrite -(eq_map (fun e => interp_ext _ _ e Hl)). rewrite Hl. apply continuity_pt_ext => x. apply interp_ext => k. rewrite 2!nth_set_nth /=. now case eqtype.eq_op. rewrite 2!Hl. apply continuity_2d_pt_ext => x y. apply interp_ext => k. rewrite 2!nth_set_nth /=. case eqtype.eq_op => //. rewrite 2!nth_set_nth /=. now case eqtype.eq_op. rewrite 2!(interp_ext _ _ _ Hl). apply ex_RInt_ext. intros x _. apply interp_ext. intros [|k]. easy. apply Hl. rewrite Hl. apply filter_imp => y. rewrite 2!(interp_ext _ _ _ Hl). apply ex_RInt_ext. intros x _. apply interp_ext. intros [|k]. easy. now rewrite /= 2!nth_set_nth /= Hl. intros (d,H). exists d. rewrite -Hl. move: H ; apply filter_imp => y. rewrite (interp_ext _ _ _ Hl). apply ex_RInt_ext. intros x _. apply interp_ext. intros [|k]. easy. now rewrite /= 2!nth_set_nth /= Hl. induction ld. easy. simpl in H |- *. intros (H1,H2). split. apply (proj1 H _ _ Hl H1). now apply IHld. rewrite 2!(interp_ext _ _ _ Hl). intros H t Ht. apply (IHb (t :: l1)). intros [|k]. easy. apply Hl. now apply H. apply IHb. intros [|k]. now apply interp_ext. apply Hl. rewrite Hl. apply filter_imp => y. apply IHb => k. now rewrite 2!nth_set_nth /= Hl. rewrite 2!Hl. apply locally_2d_impl. apply locally_2d_forall => u v. apply IHb => k. rewrite 2!nth_set_nth /=. case eqtype.eq_op => //. rewrite 2!nth_set_nth /=. now case eqtype.eq_op. rewrite Hl 2!(interp_ext _ _ _ Hl). intros (d,Hd). exists d => t u Ht Hu. apply: IHb (Hd t u Ht Hu). intros [|k]. easy. now rewrite /= 2!nth_set_nth /= Hl. Qed.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct