proposition: Lemma base_indf (P : base -> Prop) : P Undef -> P empty -> (forall k v f, P f -> valid (union (pts k v) f) -> path ord (k : [ordType of K]) (dom f) -> P (union (pts k v) f)) -> forall f, P f.
proof: Proof. rewrite /empty => H1 H2 H3; apply: base_ind=>//. apply: fmap_ind'=>[|k v f S IH] H. - by set f := Def _ in H2; rewrite (_ : Def H = f) // /f umapE. have N : k \notin supp f by apply: notin_path S. have [T1 T2] : C k /\ all C (supp f). - split; first by apply: (allP H k); rewrite supp_ins inE /= eq_refl. - apply/allP=>x T; apply: (allP H x). by rewrite supp_ins inE /= T orbT. have E : FinMap (sorted_ins' k v (sorted_nil K V)) = ins k v (@nil K V) by []. have: valid (union (pts k v) (Def T2)). - rewrite /valid /union /pts /upd /=. case: decP; last by rewrite T1. by move=>T; case: ifP=>//; rewrite E disjC disj_ins N disj_nil. move/(H3 k v _ (IH T2)). rewrite (_ : union (pts k v) (Def T2) = Def H). - by apply. rewrite umapE /union /pts /upd /=. case: decP=>// T; rewrite /disj /= N /=. by rewrite E fcat_inss // fcat0s. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)