Require Export ListFunctions. 
 
Set Implicit Arguments.
Unset Strict Implicit. 
 
(*Definition of security class, and its standard partial order.      *) 

(*
SECLEV: security levels
CATEGORY: categories, departments or need-to-know
*)

Definition SECLEV := nat. 
Parameter CATEGORY : Set. 

(*SecClass: security class or access class*)

Record SecClass : Set := sclass {level : SECLEV; categs : set CATEGORY}. 
 
Definition eq_sc (a b : SecClass) : Prop :=
  level a = level b /\ categs a = categs b. 
 
Definition le_sc (a b : SecClass) : Prop :=
  level a <= level b /\ Included (categs a) (categs b). 
 
Hint Unfold eq_sc le_sc. 
 
 
(*********************************************************************) 
(*                  Security Policy Subjects                         *) 
(*********************************************************************) 
 
(*This are global parameters introducing the basic sets of the model.*) 

(*
SUBJECT: all the subjects of the system
GRPNAME: all the group names of the system
root: UNIX superuser
secofr: security officer, in charge of MAC attributes
*)
 
Parameter SUBJECT GRPNAME : Set. 
Parameter root secofr : SUBJECT. 
 
 
(*These axioms are needed by functions of ListSet.                   *) 
 
Axiom SUBeq_dec : forall x y : SUBJECT, {x = y} + {x <> y}. 
Axiom GRPeq_dec : forall x y : GRPNAME, {x = y} + {x <> y}. 
 
Hint Resolve SUBeq_dec GRPeq_dec. 
 
 
(*********************************************************************) 
(*                         The Filesystem                            *) 
(*********************************************************************) 
 
(*
OBJNAME: all the possible absolute path names for files and directories
BYTE: elements that can be stored in a file
*) 

Parameter OBJNAME BYTE : Set. 
 
 
(*These axioms are needed by functions of ListSet.                   *) 
Axiom OBJNAMEeq_dec : forall x y : OBJNAME, {x = y} + {x <> y}. 
Axiom BYTEeq_dec : forall x y : BYTE, {x = y} + {x <> y}. 
 
Hint Resolve OBJNAMEeq_dec BYTEeq_dec. 
 
 
(*OBJTYPE: used to distinguish between files and directories*)

Inductive OBJTYPE : Set :=
  | File : OBJTYPE
  | Directory : OBJTYPE. 
 
Lemma OBJTYPEeq_dec : forall x y : OBJTYPE, {x = y} + {x <> y}. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: sumbool (@eq OBJTYPE x y) (not (@eq OBJTYPE x y)) *)
elim x; elim y. 
(* Goal: or (@eq X x x) False *)
(* Goal: @set_In X x (DOM (@set_add (prod X Y) XYeq_dec (@pair X Y x y) (@cons (prod X Y) a f))) *)
left; auto. 
 
(* Goal: sumbool (@eq OBJTYPE Directory File) (not (@eq OBJTYPE Directory File)) *)
(* Goal: sumbool (@eq OBJTYPE Directory Directory) (not (@eq OBJTYPE Directory Directory)) *)
right; intro; discriminate H. 
 
(* Goal: sumbool (@eq OBJTYPE Directory File) (not (@eq OBJTYPE Directory File)) *)
(* Goal: sumbool (@eq OBJTYPE Directory Directory) (not (@eq OBJTYPE Directory Directory)) *)
right; intro; discriminate H. 
 
(* Goal: or (@eq X x x) False *)
(* Goal: @set_In X x (DOM (@set_add (prod X Y) XYeq_dec (@pair X Y x y) (@cons (prod X Y) a f))) *)
left; auto. 
 
Qed. 
 
Hint Resolve OBJTYPEeq_dec. 
 
 
(*FILECONT: all the possible contents of files*)

Definition FILECONT := list BYTE. 
 
Lemma FILECONTeq_dec : forall x y : FILECONT, {x = y} + {x <> y}. 
(* Goal: forall x y : FILECONT, sumbool (@eq FILECONT x y) (not (@eq FILECONT x y)) *)
unfold FILECONT in |- *; intros; apply Listeq_dec. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
Hint Resolve FILECONTeq_dec. 
 
 
(*DIRCONT: all the possible contents of directories*)

Definition DIRCONT := list OBJNAME. 

Lemma DIRCONTeq_dec : forall x y : DIRCONT, {x = y} + {x <> y}. 
(* Goal: forall x y : DIRCONT, sumbool (@eq DIRCONT x y) (not (@eq DIRCONT x y)) *)
unfold DIRCONT in |- *; intros; apply Listeq_dec. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
Hint Resolve DIRCONTeq_dec. 
 

Definition OBJECT := (OBJNAME * OBJTYPE)%type. 
 
Lemma OBJeq_dec : forall x y : OBJECT, {x = y} + {x <> y}. 
(* Goal: forall x y : OBJECT, sumbool (@eq OBJECT x y) (not (@eq OBJECT x y)) *)
unfold OBJECT in |- *. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
apply Prodeq_dec; auto. 
Qed. 
 
(*MyDir(o): parent directory of object o*)

Parameter MyDir : OBJNAME -> OBJECT. 
 
Definition ObjName (o : OBJECT) : OBJNAME := fst o. 
 
Definition ObjType (o : OBJECT) : OBJTYPE := snd o. 
 
 
(*********************************************************************) 
(*                  Security Policy Objects                          *) 
(*********************************************************************) 
 
(*
(allowedTo a b):
 if a pattern-matches (PM) true, then read access is allowed; otherwise it isn'
 if b PM true, then write access is allowed; otherwise it isn't
*)
 
Record RIGHTS : Set := allowedTo {read_right : bool; write_right : bool}. 


(*
(rwx o g a):
 if o PM (allowedTo x y) then the owner has or has't read and/or write access;
 if g PM (allowedTo x y) then group g has or has't read and/or write access;
 if a PM (allowedTo x y) then all the system subjects has or has't read and/or write access
*)
 
Record PERMS : Set := rwx {ownerp : RIGHTS; groupp : RIGHTS; otherp : RIGHTS}. 
 
(*Designated below*)
Record AccessCtrlListData : Set := acldata
  {owner : SUBJECT;
   group : GRPNAME;
   UsersReaders : set SUBJECT;
   GroupReaders : set GRPNAME;
   UsersWriters : set SUBJECT;
   GroupWriters : set GRPNAME;
   UsersOwners : set SUBJECT;
   GroupOwners : set GRPNAME}. 
 
 
(*Designated below*)
Record ReadersWriters : Set := mkRW
  {ActReaders : set SUBJECT; ActWriters : set SUBJECT}. 
 
Axiom RWeq_dec : forall x1 x2 : ReadersWriters, {x1 = x2} + {x1 <> x2}. 
 
 
(*********************************************************************) 
(*                     Secured FileSystem                            *) 
(*********************************************************************) 
 
(*This record represents the state of the filesystem from the security point of view. Designations for each field:

(groups g): all the subjects which belong to group g

(primaryGrp s): the (UNIX) primary group of subject s

(set_In (u,sc) (subjectSC s)): iff sc is the security class of u in state s

AllGrp: group containing all the system subjects

SecAdmGrp: group of the security administrators in charge of MAC attributes

RootGrp: group of all subjects with the same access of subject root

(set_In (o,sc) (objectSC s)): iff sc is the security class of o in state s

(set_In (o,(acldata o g ur gr uw gw uo go)) (acl s)):
  iff (acldata o g ur gr uw gw uo go) is the ACL of o in state s, in that case:
   o is the UNIX owner of o,
   g is the UNIX group of o,
   ur is a set of subjects with read access to o,
   gr is a set of groups with read access to o,
   uw is a set of subjects with write access to o,
   gw is a set of groups with write access to o,
   uo is a set of subjects which are owners of o,
   go is a set of groups wich are owners of o.

(set_In (o, (mkRW ar aw)) (secmat s): 
 iff (mkRW ar aw) are the subjects accessing object o in state s, in that case:
  ar: subjects reading from o
  aw: subjects writing into o

(set_In (f,fc) (files s)): iff file name f with file content fc is stored in the file system in state s

(set_In (f,dc) (directories s)): iff directory name d with directory content dc is stored in the filesystem in state s.
*)

Record SFSstate : Set := mkSFS
  {groups : GRPNAME -> set SUBJECT;
   primaryGrp : SUBJECT -> GRPNAME;
   subjectSC : set (SUBJECT * SecClass);
   AllGrp : GRPNAME;
   RootGrp : GRPNAME;
   SecAdmGrp : GRPNAME;
   objectSC : set (OBJECT * SecClass);
   acl : set (OBJECT * AccessCtrlListData);
   secmat : set (OBJECT * ReadersWriters);
   files : set (OBJECT * FILECONT);
   directories : set (OBJECT * DIRCONT)}. 
 
 
(*Axioms needed for decidability                                     *) 
Axiom SSCeq_dec : forall x1 x2 : SUBJECT * SecClass, {x1 = x2} + {x1 <> x2}. 
Axiom OSCeq_dec : forall x1 x2 : OBJECT * SecClass, {x1 = x2} + {x1 <> x2}. 
Axiom
  ACLeq_dec :
    forall x1 x2 : OBJECT * AccessCtrlListData, {x1 = x2} + {x1 <> x2}. 
Axiom
  SECMATeq_dec :
    forall x1 x2 : OBJECT * ReadersWriters, {x1 = x2} + {x1 <> x2}. 
Axiom OBJFeq_dec : forall x1 x2 : OBJECT * FILECONT, {x1 = x2} + {x1 <> x2}. 
Axiom OBJDeq_dec : forall x1 x2 : OBJECT * DIRCONT, {x1 = x2} + {x1 <> x2}. 
 
Hint Resolve SSCeq_dec OSCeq_dec ACLeq_dec SECMATeq_dec RWeq_dec. 
 
 

(*In this section we implement finite partial functions (FPF) with type set defined at module ListSet.v.

A FPF is a set of pairs. Given that both (x,y1) and (x,y2) with y1 != y2 may belong to a set of pairs, not every set of pairs is a FPF. For this reason, the specifier should use function IsPARTFUNC to test whether a given set of pairs is a FPF or not. All the other functions (DOM, RAN and PARTFUNC) assume that this test has been performed, otherwise their results are usless.

If f is a FPF and (x,y) belongs to f, then
 -f applied to x yields y,
 -x belongs to the domain of f
 -y belongs to the range of f.
*)
 
Section PartialFunctions.

Variable X Y : Set. 
 
Hypothesis Xeq_dec : forall x1 x2 : X, {x1 = x2} + {x1 <> x2}. 
Hypothesis Yeq_dec : forall x1 x2 : Y, {x1 = x2} + {x1 <> x2}. 
Hypothesis XYeq_dec : forall x1 x2 : X * Y, {x1 = x2} + {x1 <> x2}. 

(*Domain of a FPF*)
Fixpoint DOM (f : set (X * Y)) : set X :=
  match f with
  | nil => nil (A:=X)
  | (x, y) :: g => set_add Xeq_dec x (DOM g)
  end. 

(*Range of a FPF*)
Fixpoint RAN (f : set (X * Y)) : set Y :=
  match f with
  | nil => nil (A:=Y)
  | (x, y) :: g => set_add Yeq_dec y (RAN g)
  end. 

(*Application of a FPF*)
Fixpoint PARTFUNC (f : set (X * Y)) : X -> Exc Y :=
  fun x : X =>
  match f with
  | nil => None (A:=Y)
  | (x1, y) :: g =>
      match Xeq_dec x x1 with
      | left _ => Some y
      | right _ => PARTFUNC g x
      end
  end. 
 
(*Test to decide whether a set of pairs is a FPF or not*)
Fixpoint IsPARTFUNC (f : set (X * Y)) : Prop :=
  match f with
  | nil => True
  | a :: l =>
      match set_In_dec Xeq_dec (fst a) (DOM l) with
      | left _ => False
      | right _ => IsPARTFUNC l
      end
  end. 
 
(*Some usefull lemmas about our implementation of FPF*)

Lemma AddEq :
 forall (a b : X) (y : Y) (f : set (X * Y)),
 a <> b -> PARTFUNC f a = PARTFUNC (set_add XYeq_dec (b, y) f) a. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
induction  f as [| a0 f Hrecf]. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (@None Y) (if Xeq_dec a b then @Some Y z else @None Y) *)
(* Goal: @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a0 f) a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) (@cons (prod X Y) a0 f))) a) *)
elim (Xeq_dec a b). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro. 
(* Goal: @eq (Exc Y) (@None Y) (@Some Y y) *)
(* Goal: False *)
(* Goal: forall _ : not (@eq X a b), @eq (Exc Y) (@None Y) (@None Y) *)
(* Goal: @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a0 f) a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b y) (@cons (prod X Y) a0 f)) a) *)
elim H0. 
 
(* Goal: False *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
unfold not in H; apply H. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (let (x1, y) := a0 in if Xeq_dec a x1 then @Some Y y else PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) a0 then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) a0 (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim a0. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim (XYeq_dec (b, y) (a1, b0)). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : False, @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
elim F. 
 
(* Goal: False *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
unfold not in H. 
(* Goal: @eq (list (prod X Y)) l (@set_remove (prod X Y) XYeq_dec (@pair X Y a2 b0) l) *)
apply H. 
(* Goal: @eq X a b *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
rewrite a3. 
(* Goal: @eq X a1 b *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
injection a2. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : False, @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim (XYeq_dec (b, y) (a1, b0)). 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : False, @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : False, @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
 
Lemma AddEq1 :
 forall (x : X) (y : Y) (f : set (X * Y)),
 ~ set_In x (DOM f) -> value y = PARTFUNC (set_add XYeq_dec (x, y) f) x. 
(* Goal: forall (x : X) (y : Y) (f : set (prod X Y)) (_ : IsPARTFUNC f) (_ : @set_In (prod X Y) (@pair X Y x y) f), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) f) x) (@None Y) *)
simple induction f. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim (Xeq_dec x x); auto. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro; absurd (x = x); auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (a : prod X Y) (l : list (prod X Y)) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : if @set_In_dec X Xeq_dec (@fst X Y a) (DOM l) then False else IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (if XYeq_dec (@pair X Y x y) a then @set_remove (prod X Y) XYeq_dec (@pair X Y x y) l else @cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
intros until l. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim a. 
(* Goal: forall (a : X) (b : Y) (_ : forall _ : not (@set_In X x (DOM l)), @eq (option Y) (@value Y y) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y x y) l) x)) (_ : not (@set_In X x (@set_add X Xeq_dec a (DOM l)))), @eq (option Y) (@value Y y) (PARTFUNC (if XYeq_dec (@pair X Y x y) (@pair X Y a b) then @cons (prod X Y) (@pair X Y a b) l else @cons (prod X Y) (@pair X Y a b) (@set_add (prod X Y) XYeq_dec (@pair X Y x y) l)) x) *)
intros until b. 
(* Goal: forall (_ : forall _ : not (@set_In X x (DOM l)), @eq (option Y) (@value Y y) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y x y) l) x)) (_ : not (@set_In X x (@set_add X Xeq_dec a0 (DOM l)))), @eq (option Y) (@value Y y) (PARTFUNC (if XYeq_dec (@pair X Y x y) (@pair X Y a0 b) then @cons (prod X Y) (@pair X Y a0 b) l else @cons (prod X Y) (@pair X Y a0 b) (@set_add (prod X Y) XYeq_dec (@pair X Y x y) l)) x) *)
elim (XYeq_dec (x, y) (a0, b)). 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim (Xeq_dec x a0). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
injection a2; intros. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
rewrite H1; auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
injection a1; intros; absurd (x = a0); auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim (Xeq_dec x a0). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (option Y) (@value Y y) (@Some Y b) *)
(* Goal: forall (_ : not (@eq X x a0)) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a0 b))) (_ : forall _ : not (@set_In X x (DOM l)), @eq (option Y) (@value Y y) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y x y) l) x)) (_ : not (@set_In X x (@set_add X Xeq_dec a0 (DOM l)))), @eq (option Y) (@value Y y) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y x y) l) x) *)
rewrite a1 in H0. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
tauto. 
 
(* Goal: False *)
(* Goal: forall (_ : not (@eq X o a0)) (_ : not (@set_In X o (@set_add X Xeq_dec a0 (DOM f)))), @eq (Exc Y) (PARTFUNC f o) (@None Y) *)
apply H0. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
apply set_add_intro2; auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (list (prod X Y)) l (@set_remove (prod X Y) XYeq_dec (@pair X Y a2 b0) l) *)
apply H. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro; apply H0; apply set_add_intro1; auto. 
 
Qed. 
 
 
Lemma RemEq :
 forall (a b : X) (y : Y) (f : set (X * Y)),
 a <> b -> PARTFUNC f a = PARTFUNC (set_remove XYeq_dec (b, y) f) a. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
induction  f as [| a0 f Hrecf].
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto.

(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (let (x1, y) := a0 in if Xeq_dec a x1 then @Some Y y else PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) a0 then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) a0 (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim a0. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim (XYeq_dec (b, y) (a1, b0)). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : False, @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
elim F. 
 
(* Goal: False *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
unfold not in H. 
(* Goal: @eq (list (prod X Y)) l (@set_remove (prod X Y) XYeq_dec (@pair X Y a2 b0) l) *)
apply H. 
(* Goal: @eq X a b *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
rewrite a3. 
(* Goal: @eq X a1 b *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
injection a2. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : False, @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim (XYeq_dec (b, y) (a1, b0)). 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : False, @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : False, @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
 
Lemma AddRemEq :
 forall (a b : X) (y z : Y) (f : set (X * Y)),
 a <> b ->
 PARTFUNC f a =
 PARTFUNC (set_add XYeq_dec (b, z) (set_remove XYeq_dec (b, y) f)) a. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
induction  f as [| a0 f Hrecf]. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (@None Y) (if Xeq_dec a b then @Some Y z else @None Y) *)
(* Goal: @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a0 f) a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) (@cons (prod X Y) a0 f))) a) *)
elim (Xeq_dec a b). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F; elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (let (x1, y) := a0 in if Xeq_dec a x1 then @Some Y y else PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) a0 then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) a0 (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim a0. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim (XYeq_dec (b, y) (a1, b0)). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F; elim F. 
 
(* Goal: False *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
unfold not in H; apply H. 
(* Goal: @eq X a b *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
rewrite a3. 
(* Goal: @eq X a1 b *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
injection a2. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (if XYeq_dec (@pair X Y b z) (@pair X Y a1 b0) then @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) else @cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim (XYeq_dec (b, z) (a1, b0)). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F; elim F. 
 
(* Goal: False *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
unfold not in H. 
(* Goal: @eq (list (prod X Y)) l (@set_remove (prod X Y) XYeq_dec (@pair X Y a2 b0) l) *)
apply H. 
(* Goal: @eq X a b *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
rewrite a3. 
(* Goal: @eq X a1 b *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0))) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : @eq X a a1), @eq (Exc Y) (@Some Y b0) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
injection a2. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F; elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X a a1), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) (@pair X Y a1 b0) then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim (XYeq_dec (b, y) (a1, b0)). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (if XYeq_dec (@pair X Y b z) (@pair X Y a1 b0) then @cons (prod X Y) (@pair X Y a1 b0) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) else @cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
elim (XYeq_dec (b, z) (a1, b0)). 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F; elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@cons (prod X Y) (@pair X Y a1 b0) (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
apply RemEq. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq (prod X Y) (@pair X Y b z) (@pair X Y a1 b0)), @eq (Exc Y) (PARTFUNC f a) (if Xeq_dec a a1 then @Some Y b0 else PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f)) a) *)
elim (Xeq_dec a a1). 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F; elim F. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
 
Lemma NotInDOMIsUndef :
 forall (o : X) (f : set (X * Y)), ~ set_In o (DOM f) -> PARTFUNC f o = None. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
induction  f as [| a f Hrecf]. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a f) o) (@None Y) *)
generalize H. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim a. 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro; intro. 
(* Goal: forall (b : Y) (l : list (prod X Y)) (_ : forall _ : @set_In X o (DOM l), not (@eq (Exc Y) (PARTFUNC l o) (@None Y))) (_ : @set_In X o (@set_add X Xeq_dec a0 (DOM l))), not (@eq (Exc Y) (if Xeq_dec o a0 then @Some Y b else PARTFUNC l o) (@None Y)) *)
elim (Xeq_dec o a0). 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro. 
(* Goal: forall _ : not (@set_In X o (@set_add X Xeq_dec a0 (DOM f))), @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall (_ : not (@eq X o a0)) (_ : not (@set_In X o (@set_add X Xeq_dec a0 (DOM f)))), @eq (Exc Y) (PARTFUNC f o) (@None Y) *)
rewrite a1. 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: @eq (Exc Y) (PARTFUNC f a) (@Some Y b0) *)
(* Goal: False *)
(* Goal: forall (_ : not (@eq X a a1)) (_ : not (@eq (prod X Y) (@pair X Y b y) (@pair X Y a1 b0))) (_ : not (@eq X a a1)), @eq (Exc Y) (PARTFUNC f a) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f) a) *)
intro F; elim F. 
 
(* Goal: False *)
(* Goal: forall (_ : not (@eq X o a0)) (_ : not (@set_In X o (@set_add X Xeq_dec a0 (DOM f)))), @eq (Exc Y) (PARTFUNC f o) (@None Y) *)
unfold not in H0. 
(* Goal: False *)
(* Goal: forall (_ : not (@eq X o a0)) (_ : not (@set_In X o (@set_add X Xeq_dec a0 (DOM f)))), @eq (Exc Y) (PARTFUNC f o) (@None Y) *)
apply H0. 
(* Goal: @set_In X a0 (@set_add X Xeq_dec a0 (DOM f)) *)
(* Goal: forall (_ : not (@eq X o a0)) (_ : not (@set_In X o (@set_add X Xeq_dec a0 (DOM f)))), @eq (Exc Y) (PARTFUNC f o) (@None Y) *)
apply set_add_intro2. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (PARTFUNC f o) (@None Y) *)
apply Hrecf. 
(* Goal: not (@set_In X o (DOM f)) *)
unfold not in H0; unfold not in |- *. 
(* Goal: False *)
(* Goal: forall (_ : not (@eq X o a0)) (_ : not (@set_In X o (@set_add X Xeq_dec a0 (DOM f)))), @eq (Exc Y) (PARTFUNC f o) (@None Y) *)
intro; apply H0. 
(* Goal: @set_In X o (@set_add X Xeq_dec a0 (DOM f)) *)
apply set_add_intro1. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
Hint Resolve NotInDOMIsUndef.    
 
Lemma InDOMIsNotUndef :
 forall (o : X) (f : set (X * Y)), set_In o (DOM f) -> PARTFUNC f o <> None. 
(* Goal: forall (x : X) (y : Y) (f : set (prod X Y)) (_ : IsPARTFUNC f) (_ : @set_In (prod X Y) (@pair X Y x y) f), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) f) x) (@None Y) *)
simple induction f. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim a. 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro. 
(* Goal: forall (b : Y) (l : list (prod X Y)) (_ : forall _ : @set_In X o (DOM l), not (@eq (Exc Y) (PARTFUNC l o) (@None Y))) (_ : @set_In X o (@set_add X Xeq_dec a0 (DOM l))), not (@eq (Exc Y) (if Xeq_dec o a0 then @Some Y b else PARTFUNC l o) (@None Y)) *)
elim (Xeq_dec o a0). 
(* Goal: forall (_ : @eq X o a0) (b : Y) (l : list (prod X Y)) (_ : forall _ : @set_In X o (DOM l), not (@eq (Exc Y) (PARTFUNC l o) (@None Y))) (_ : @set_In X o (@set_add X Xeq_dec a0 (DOM l))), not (@eq (Exc Y) (@Some Y b) (@None Y)) *)
(* Goal: forall (_ : not (@eq X o a0)) (_ : Y) (l : list (prod X Y)) (_ : forall _ : @set_In X o (DOM l), not (@eq (Exc Y) (PARTFUNC l o) (@None Y))) (_ : @set_In X o (@set_add X Xeq_dec a0 (DOM l))), not (@eq (Exc Y) (PARTFUNC l o) (@None Y)) *)
intros; intro H3; discriminate H3. 
 
(* Goal: @eq (list (prod X Y)) l (@set_remove (prod X Y) XYeq_dec (@pair X Y a2 b0) l) *)
intros; apply H. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
eauto. 
 
Qed. 
 
 
Lemma InDOMWhenAdd :
 forall (x : X) (y : Y) (f : set (X * Y)),
 set_In x (DOM (set_add XYeq_dec (x, y) f)). 
intros; induction  f as [| a f Hrecf]. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: or (@eq X x x) False *)
(* Goal: @set_In X x (DOM (@set_add (prod X Y) XYeq_dec (@pair X Y x y) (@cons (prod X Y) a f))) *)
left; auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @set_In X x (DOM (if XYeq_dec (@pair X Y x y) a then @cons (prod X Y) a f else @cons (prod X Y) a (@set_add (prod X Y) XYeq_dec (@pair X Y x y) f))) *)
elim (XYeq_dec (x, y) a). 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim a. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
injection a1; intros. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
apply set_add_intro2; auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim a. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
apply set_add_intro1; auto. 
 
Qed. 
 
 
Lemma DOMFuncRel :
 forall (a : X * Y) (f : set (X * Y)),
 ~ set_In (fst a) (DOM f) -> f = set_remove XYeq_dec a f. 
(* Goal: forall (x : X) (y : Y) (f : set (prod X Y)) (_ : IsPARTFUNC f) (_ : @set_In (prod X Y) (@pair X Y x y) f), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) f) x) (@None Y) *)
simple induction f. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
simpl in |- *; auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: @eq (Exc Y) (let (x1, y) := a0 in if Xeq_dec a x1 then @Some Y y else PARTFUNC f a) (PARTFUNC (@set_add (prod X Y) XYeq_dec (@pair X Y b z) (if XYeq_dec (@pair X Y b y) a0 then @set_remove (prod X Y) XYeq_dec (@pair X Y b y) f else @cons (prod X Y) a0 (@set_remove (prod X Y) XYeq_dec (@pair X Y b y) f))) a) *)
intro; elim a0. 
(* Goal: forall (a0 : X) (b : Y) (l : list (prod X Y)) (_ : forall _ : not (@set_In X (@fst X Y a) (DOM l)), @eq (set (prod X Y)) l (@set_remove (prod X Y) XYeq_dec a l)) (_ : not (@set_In X (@fst X Y a) (@set_add X Xeq_dec a0 (DOM l)))), @eq (set (prod X Y)) (@cons (prod X Y) (@pair X Y a0 b) l) (if XYeq_dec a (@pair X Y a0 b) then @set_remove (prod X Y) XYeq_dec a l else @cons (prod X Y) (@pair X Y a0 b) (@set_remove (prod X Y) XYeq_dec a l)) *)
intros until b; elim (XYeq_dec a (a1, b)). 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim a. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
injection a3; intros. 
(* Goal: @eq (set (prod X Y)) (@cons (prod X Y) (@pair X Y a1 b) l) (@set_remove (prod X Y) XYeq_dec (@pair X Y a2 b0) l) *)
(* Goal: forall (_ : not (@eq (prod X Y) a (@pair X Y a1 b))) (l : list (prod X Y)) (_ : forall _ : not (@set_In X (@fst X Y a) (DOM l)), @eq (set (prod X Y)) l (@set_remove (prod X Y) XYeq_dec a l)) (_ : not (@set_In X (@fst X Y a) (@set_add X Xeq_dec a1 (DOM l)))), @eq (set (prod X Y)) (@cons (prod X Y) (@pair X Y a1 b) l) (@cons (prod X Y) (@pair X Y a1 b) (@set_remove (prod X Y) XYeq_dec a l)) *)
simpl in H0; rewrite H2 in H0. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
tauto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
apply H0; apply set_add_intro2; auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim a. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (set (prod X Y)) (@cons (prod X Y) (@pair X Y a1 b) l) (@cons (prod X Y) (@pair X Y a1 b) (@set_remove (prod X Y) XYeq_dec (@pair X Y a2 b0) l)) *)
cut (l = set_remove XYeq_dec (a2, b0) l). 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
rewrite <- H1; auto. 
 
(* Goal: @eq (list (prod X Y)) l (@set_remove (prod X Y) XYeq_dec (@pair X Y a2 b0) l) *)
apply H. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro; apply H0; apply set_add_intro; auto. 
 
Qed. 
 
Hint Resolve DOMFuncRel. 
 
 
Lemma DOMFuncRel2 :
 forall (z : X * Y) (f : set (X * Y)), set_In z f -> set_In (fst z) (DOM f). 
(* Goal: forall (x : X) (y : Y) (f : set (prod X Y)) (_ : IsPARTFUNC f) (_ : @set_In (prod X Y) (@pair X Y x y) f), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) f) x) (@None Y) *)
simple induction f. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
simpl in |- *; auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro; elim a. 
(* Goal: forall (a : X) (b : Y) (l : list (prod X Y)) (_ : forall _ : @set_In (prod X Y) z l, @set_In X (@fst X Y z) (DOM l)) (_ : or (@eq (prod X Y) (@pair X Y a b) z) (@set_In (prod X Y) z l)), @set_In X (@fst X Y z) (@set_add X Xeq_dec a (DOM l)) *)
elim z. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim H0; intro. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
injection H1; intros. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
apply set_add_intro; auto. 
 
(* Goal: @set_In X a0 (@set_add X Xeq_dec a1 (DOM l)) *)
cut (set_In a0 (DOM l)). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro; apply set_add_intro1; auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
Hint Resolve DOMFuncRel2. 
 
 
Lemma DOMFuncRel3 :
 forall (x : X) (y : Y) (f : set (X * Y)),
 IsPARTFUNC f ->
 set_In (x, y) f -> ~ set_In x (DOM (set_remove XYeq_dec (x, y) f)). 
(* Goal: forall (x : X) (y : Y) (f : set (prod X Y)) (_ : IsPARTFUNC f) (_ : @set_In (prod X Y) (@pair X Y x y) f), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) f) x) (@None Y) *)
simple induction f. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
simpl in |- *; auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
intros until l; elim (set_In_dec Xeq_dec (fst a) (DOM l));
(* Goal: @set_In X x (DOM (if XYeq_dec (@pair X Y x y) a then @cons (prod X Y) a f else @cons (prod X Y) a (@set_add (prod X Y) XYeq_dec (@pair X Y x y) f))) *)
 elim (XYeq_dec (x, y) a). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
tauto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
tauto. 
 
(* Goal: forall (_ : @eq (prod X Y) (@pair X Y x y) a) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), not (@set_In X x (DOM (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)))) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), not (@set_In X x (DOM (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l))) *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), not (@set_In X x (DOM (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)))) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), not (@set_In X x (DOM (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)))) *)
intros; cut (l = set_remove XYeq_dec (x, y) l). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro H2; rewrite <- H2; replace x with (fst a); auto. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
rewrite <- a0; auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
rewrite a0; auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim a. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim H1; intro. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
absurd ((a0, b) = (x, y)); auto. 
 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim (Xeq_dec x a0); intro. 
(* Goal: @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
rewrite <- a1 in b1. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro; apply b1; replace x with (fst (x, y)); auto. 
 
(* Goal: not (@set_In X x (@set_add X Xeq_dec a0 (DOM (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)))) *)
cut (~ set_In x (DOM (set_remove XYeq_dec (x, y) l))). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
 
Lemma DOMFuncRel4 :
 forall (x : X) (f : set (X * Y)),
 match PARTFUNC f x with
 | Some a => set_In (x, a) f
 | None => ~ set_In x (DOM f)
 end. 
(* Goal: forall (x : X) (y : Y) (f : set (prod X Y)) (_ : IsPARTFUNC f) (_ : @set_In (prod X Y) (@pair X Y x y) f), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) f) x) (@None Y) *)
simple induction f. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
simpl in |- *; auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros until l; elim a. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros until b; elim (Xeq_dec x a0). 
(* Goal: forall (_ : not (@eq X x a0)) (_ : match PARTFUNC l x with | Some a => @set_In (prod X Y) (@pair X Y x a) l | None => not (@set_In X x (DOM l)) end), match PARTFUNC l x with | Some a => or (@eq (prod X Y) (@pair X Y a0 b) (@pair X Y x a)) (@set_In (prod X Y) (@pair X Y x a) l) | None => not (@set_In X x (@set_add X Xeq_dec a0 (DOM l))) end *)
elim (PARTFUNC l x). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros y2 H; left; rewrite H; auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros H H1; left; rewrite H; auto. 
 
(* Goal: forall (_ : not (@eq X x a0)) (_ : match PARTFUNC l x with | Some a => @set_In (prod X Y) (@pair X Y x a) l | None => not (@set_In X x (DOM l)) end), match PARTFUNC l x with | Some a => or (@eq (prod X Y) (@pair X Y a0 b) (@pair X Y x a)) (@set_In (prod X Y) (@pair X Y x a) l) | None => not (@set_In X x (@set_add X Xeq_dec a0 (DOM l))) end *)
elim (PARTFUNC l x). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
 
Lemma UndefWhenRem :
 forall (x : X) (y : Y) (f : set (X * Y)),
 IsPARTFUNC f ->
 set_In (x, y) f -> PARTFUNC (set_remove XYeq_dec (x, y) f) x = None. 
(* Goal: forall (x : X) (y : Y) (f : set (prod X Y)) (_ : IsPARTFUNC f) (_ : @set_In (prod X Y) (@pair X Y x y) f), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) f) x) (@None Y) *)
simple induction f. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
simpl in |- *; auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (a : prod X Y) (l : list (prod X Y)) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : if @set_In_dec X Xeq_dec (@fst X Y a) (DOM l) then False else IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (if XYeq_dec (@pair X Y x y) a then @set_remove (prod X Y) XYeq_dec (@pair X Y x y) l else @cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
intros until l. 
(* Goal: @set_In X x (DOM (if XYeq_dec (@pair X Y x y) a then @cons (prod X Y) a f else @cons (prod X Y) a (@set_add (prod X Y) XYeq_dec (@pair X Y x y) f))) *)
elim (set_In_dec Xeq_dec (fst a) (DOM l)); elim (XYeq_dec (x, y) a). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
tauto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
tauto. 
 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
replace (set_remove XYeq_dec (x, y) l) with l. 
(* Goal: @eq (list (prod X Y)) l (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
rewrite <- a0 in b. 
(* Goal: @eq (Exc Y) (PARTFUNC l x) (@None Y) *)
(* Goal: @eq (list (prod X Y)) l (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in b. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: @eq (list (prod X Y)) l (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) *)
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
rewrite <- a0 in b. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (PARTFUNC (@cons (prod X Y) a (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l)) x) (@None Y) *)
simpl in |- *. 
(* Goal: forall (_ : not (@eq (prod X Y) (@pair X Y x y) a)) (_ : not (@set_In X (@fst X Y a) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) a (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (let (x1, y0) := a in if Xeq_dec x x1 then @Some Y y0 else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim a. 
(* Goal: forall (a : X) (b : Y) (_ : not (@eq (prod X Y) (@pair X Y x y) (@pair X Y a b))) (_ : not (@set_In X (@fst X Y (@pair X Y a b)) (DOM l))) (_ : forall (_ : IsPARTFUNC l) (_ : @set_In (prod X Y) (@pair X Y x y) l), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y)) (_ : IsPARTFUNC l) (_ : or (@eq (prod X Y) (@pair X Y a b) (@pair X Y x y)) (@set_In (prod X Y) (@pair X Y x y) l)), @eq (Exc Y) (if Xeq_dec x a then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intros. 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim H1; intro. 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
cut False. 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
tauto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
apply b0; symmetry  in |- *; auto. 
 
(* Goal: @eq (Exc Y) (if Xeq_dec x a0 then @Some Y b else PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
elim (Xeq_dec x a0). 
(* Goal: forall _ : @eq X x a0, @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
intro. 
(* Goal: @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
simpl in b1. 
(* Goal: @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
rewrite <- a1 in b1. 
(* Goal: @eq (Exc Y) (@Some Y b) (@None Y) *)
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
absurd (set_In x (DOM l)). 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
replace x with (fst (x, y)); auto. 
 
(* Goal: forall _ : not (@eq X x a0), @eq (Exc Y) (PARTFUNC (@set_remove (prod X Y) XYeq_dec (@pair X Y x y) l) x) (@None Y) *)
auto. 
 
Qed. 
 
End PartialFunctions. 
 
Hint Resolve AddEq RemEq AddRemEq NotInDOMIsUndef InDOMIsNotUndef
  InDOMWhenAdd UndefWhenRem AddEq1 DOMFuncRel3. 
 
 
 
(*Shorthands for domains and partial functions defined for each of the state's*) 
(*components.                                                        *) 
Definition domf (f : set (OBJECT * FILECONT)) := DOM OBJeq_dec f. 
 
Definition ffiles (f : set (OBJECT * FILECONT)) : OBJECT -> Exc FILECONT :=
  PARTFUNC OBJeq_dec f. 
 
Definition domd (f : set (OBJECT * DIRCONT)) := DOM OBJeq_dec f. 
 
Definition fdirs (f : set (OBJECT * DIRCONT)) : OBJECT -> Exc DIRCONT :=
  PARTFUNC OBJeq_dec f. 
 
Definition domacl (f : set (OBJECT * AccessCtrlListData)) := DOM OBJeq_dec f. 
 
Definition facl (f : set (OBJECT * AccessCtrlListData)) :
  OBJECT -> Exc AccessCtrlListData := PARTFUNC OBJeq_dec f. 
 
Definition domsecmat (f : set (OBJECT * ReadersWriters)) := DOM OBJeq_dec f. 
 
Definition ransecmat (f : set (OBJECT * ReadersWriters)) := RAN RWeq_dec f. 
 
Definition fsecmat (f : set (OBJECT * ReadersWriters)) :
  OBJECT -> Exc ReadersWriters := PARTFUNC OBJeq_dec f. 
 
Definition domOSC (f : set (OBJECT * SecClass)) := DOM OBJeq_dec f. 
 
Definition fOSC (f : set (OBJECT * SecClass)) : OBJECT -> Exc SecClass :=
  PARTFUNC OBJeq_dec f. 
 
Definition domSSC (f : set (SUBJECT * SecClass)) := DOM SUBeq_dec f. 
 
Definition fSSC (f : set (SUBJECT * SecClass)) : SUBJECT -> Exc SecClass :=
  PARTFUNC SUBeq_dec f. 
                 
 
(*Filesystem update functions.                                       *) 
Parameter create_files : SUBJECT -> OBJNAME -> set (OBJECT * FILECONT). 
Parameter create_directories : SUBJECT -> OBJNAME -> set (OBJECT * DIRCONT). 
Parameter mkdir_directories : SUBJECT -> OBJNAME -> set (OBJECT * DIRCONT). 
Parameter rmdir_directories : OBJECT -> set (OBJECT * DIRCONT). 
Parameter unlink_files : OBJECT -> set (OBJECT * FILECONT). 
Parameter unlink_directories : OBJECT -> set (OBJECT * DIRCONT). 
Parameter write_files : OBJECT -> nat -> FILECONT -> set (OBJECT * FILECONT). 
 
 
(*
READ: pure read access
WRITE: pure write access
*)
 
Inductive MODE : Set :=
  | READ : MODE
  | WRITE : MODE. 
 
 
(*The names of the system operations.                                *) 
 
Inductive Operation : Set :=
  | Aclstat : Operation
  | AddUsrGrpToAcl : Operation
  | Chmod : Operation
  | Chobjsc : Operation
  | Chown : Operation
  | Chsubsc : Operation
  | Close : Operation
  | Create : Operation
  | DelUsrGrpFromAcl : Operation
  | Mkdir : Operation
  | Open : Operation
  | Oscstat : Operation
  | Owner_Close : Operation
  | Read : Operation
  | Readdir : Operation
  | Rmdir : Operation
  | Sscstat : Operation
  | Stat : Operation
  | Unlink : Operation
  | Write : Operation.