proposition: Lemma restr_setU1 f x a: fgraph f -> ~ (inc x (domain f)) -> restr (f +s1 (J x a)) (domain f) = f.
proof: Proof. move=> fgf xdf; symmetry. have aux: fgraph (f +s1 J x a) by apply:fgraph_setU1. have sd:= (domain_S(@subsetU2l f (singleton (J x a)))). apply: fgraph_exten; [done | by apply: restr_fgraph | by aw | move=> t tdf]. by rewrite (LgV tdf) setU1_V_in. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)