Skip to content

Instantly share code, notes, and snippets.

@JasonGross

JasonGross/pushforward.v

Created December 28, 2012 04:25
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save JasonGross/4394480 to your computer and use it in GitHub Desktop.
Save JasonGross/4394480 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
pushforward.v
{S0
: forall b : C_Objects_Ex22,
path D_Edges_Ex22 U_Ex22_D (F_Functor_Ex22_ObjectOf b) ->
match b with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end |
forall (b b' : C_Objects_Ex22)
(c : path D_Edges_Ex22 U_Ex22_D (F_Functor_Ex22_ObjectOf b))
(c' : path D_Edges_Ex22 U_Ex22_D (F_Functor_Ex22_ObjectOf b'))
(g : path
(fun s d : C_Objects_Ex22 =>
match s with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C =>
match d with
| SSN_Ex22_C => unit
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
| T2_Ex22_C =>
match d with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => unit
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
end) b b'),
concatenate c
(path_compose D_Category_Ex22 F_Functor_Ex22_ObjectOf
(fun (s0 d0 : C_Objects_Ex22)
(m : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C =>
match d0 with
| SSN_Ex22_C => unit
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
| T2_Ex22_C =>
match d0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => unit
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
end) =>
match
d0 as c0
return
(match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C =>
match c0 with
| SSN_Ex22_C => unit
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
| T2_Ex22_C =>
match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => unit
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
end ->
path D_Edges_Ex22 (F_Functor_Ex22_ObjectOf s0)
(F_Functor_Ex22_ObjectOf c0))
with
| SSN_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => Empty_set
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => Empty_set
end ->
path D_Edges_Ex22 (F_Functor_Ex22_ObjectOf c0) SSN_Ex22_D)
with
| SSN_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 SSN_Ex22_D SSN_Ex22_D) with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 FirstName_Ex22_D SSN_Ex22_D)
with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 LastName_Ex22_D SSN_Ex22_D)
with
end
| Salary_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 Salary_Ex22_D SSN_Ex22_D)
with
end
| T1_Ex22_C => fun _ : unit => AddEdge NoEdges tt
| T2_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 U_Ex22_D SSN_Ex22_D) with
end
end m0
| FirstName_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => unit
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => unit
end ->
path D_Edges_Ex22 (F_Functor_Ex22_ObjectOf c0)
FirstName_Ex22_D)
with
| SSN_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 SSN_Ex22_D FirstName_Ex22_D)
with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match
x
return (path D_Edges_Ex22 FirstName_Ex22_D FirstName_Ex22_D)
with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 LastName_Ex22_D FirstName_Ex22_D)
with
end
| Salary_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 Salary_Ex22_D FirstName_Ex22_D)
with
end
| T1_Ex22_C => fun _ : unit => AddEdge NoEdges tt
| T2_Ex22_C => fun _ : unit => AddEdge NoEdges tt
end m0
| LastName_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => unit
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => unit
end ->
path D_Edges_Ex22 (F_Functor_Ex22_ObjectOf c0) LastName_Ex22_D)
with
| SSN_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 SSN_Ex22_D LastName_Ex22_D)
with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 FirstName_Ex22_D LastName_Ex22_D)
with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 LastName_Ex22_D LastName_Ex22_D)
with
end
| Salary_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 Salary_Ex22_D LastName_Ex22_D)
with
end
| T1_Ex22_C => fun _ : unit => AddEdge NoEdges tt
| T2_Ex22_C => fun _ : unit => AddEdge NoEdges tt
end m0
| Salary_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => unit
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => unit
end ->
path D_Edges_Ex22 (F_Functor_Ex22_ObjectOf c0) Salary_Ex22_D)
with
| SSN_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 SSN_Ex22_D Salary_Ex22_D)
with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 FirstName_Ex22_D Salary_Ex22_D)
with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 LastName_Ex22_D Salary_Ex22_D)
with
end
| Salary_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 Salary_Ex22_D Salary_Ex22_D)
with
end
| T1_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 U_Ex22_D Salary_Ex22_D) with
end
| T2_Ex22_C => fun _ : unit => AddEdge NoEdges tt
end m0
| T1_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end -> path D_Edges_Ex22 (F_Functor_Ex22_ObjectOf c0) U_Ex22_D)
with
| SSN_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 SSN_Ex22_D U_Ex22_D) with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 FirstName_Ex22_D U_Ex22_D)
with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 LastName_Ex22_D U_Ex22_D)
with
end
| Salary_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 Salary_Ex22_D U_Ex22_D) with
end
| T1_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 U_Ex22_D U_Ex22_D) with
end
| T2_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 U_Ex22_D U_Ex22_D) with
end
end m0
| T2_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end -> path D_Edges_Ex22 (F_Functor_Ex22_ObjectOf c0) U_Ex22_D)
with
| SSN_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 SSN_Ex22_D U_Ex22_D) with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 FirstName_Ex22_D U_Ex22_D)
with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match
x return (path D_Edges_Ex22 LastName_Ex22_D U_Ex22_D)
with
end
| Salary_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 Salary_Ex22_D U_Ex22_D) with
end
| T1_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 U_Ex22_D U_Ex22_D) with
end
| T2_Ex22_C =>
fun x : Empty_set =>
match x return (path D_Edges_Ex22 U_Ex22_D U_Ex22_D) with
end
end m0
end m) g) = concatenate NoEdges c' ->
path_compose SetCat
(fun x : C_Objects_Ex22 =>
match x with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end)
(fun (s0 d0 : C_Objects_Ex22)
(m : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C =>
match d0 with
| SSN_Ex22_C => unit
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
| T2_Ex22_C =>
match d0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => unit
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
end) =>
match
d0 as c0
return
(match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C =>
match c0 with
| SSN_Ex22_C => unit
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
| T2_Ex22_C =>
match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => unit
| LastName_Ex22_C => unit
| Salary_Ex22_C => unit
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end
end ->
match s0 with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end ->
match c0 with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end)
with
| SSN_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => Empty_set
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => Empty_set
end ->
match c0 with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end -> SSN)
with
| SSN_Ex22_C =>
fun x : Empty_set => match x return (SSN -> SSN) with
end
| FirstName_Ex22_C =>
fun x : Empty_set => match x return (FirstName -> SSN) with
end
| LastName_Ex22_C =>
fun x : Empty_set => match x return (LastName -> SSN) with
end
| Salary_Ex22_C =>
fun x : Empty_set => match x return (Salary -> SSN) with
end
| T1_Ex22_C =>
fun (_ : unit) (id : T1_Id_Ex222) =>
SSN_intro
match id with
| x11_Ex222 => "101-22-0411"
| x12_Ex222 => "220-39-7479"
| x13_Ex222 => "775-33-2819"
end
| T2_Ex22_C =>
fun x : Empty_set => match x return (T2_Id_Ex222 -> SSN) with
end
end m0
| FirstName_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => unit
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => unit
end ->
match c0 with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end -> FirstName)
with
| SSN_Ex22_C =>
fun x : Empty_set => match x return (SSN -> FirstName) with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match x return (FirstName -> FirstName) with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match x return (LastName -> FirstName) with
end
| Salary_Ex22_C =>
fun x : Empty_set => match x return (Salary -> FirstName) with
end
| T1_Ex22_C =>
fun (_ : unit) (id : T1_Id_Ex222) =>
FirstName_intro
match id with
| x11_Ex222 => "David"
| x12_Ex222 => "Bertrand"
| x13_Ex222 => "Bertrand"
end
| T2_Ex22_C =>
fun (_ : unit) (id : T2_Id_Ex222) =>
FirstName_intro
match id with
| y1_Ex222 => "David"
| y2_Ex222 => "Bertrand"
| y3_Ex222 => "Bertrand"
| y4_Ex222 => "Alan"
end
end m0
| LastName_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => unit
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => unit
| T2_Ex22_C => unit
end ->
match c0 with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end -> LastName)
with
| SSN_Ex22_C =>
fun x : Empty_set => match x return (SSN -> LastName) with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match x return (FirstName -> LastName) with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match x return (LastName -> LastName) with
end
| Salary_Ex22_C =>
fun x : Empty_set => match x return (Salary -> LastName) with
end
| T1_Ex22_C =>
fun (_ : unit) (id : T1_Id_Ex222) =>
LastName_intro
match id with
| x11_Ex222 => "Hilbert"
| x12_Ex222 => "Russell"
| x13_Ex222 => "Russell"
end
| T2_Ex22_C =>
fun (_ : unit) (id : T2_Id_Ex222) =>
LastName_intro
match id with
| y1_Ex222 => "Hilbert"
| y2_Ex222 => "Russell"
| y3_Ex222 => "Russell"
| y4_Ex222 => "Turning"
end
end m0
| Salary_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => unit
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => unit
end ->
match c0 with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end -> Salary)
with
| SSN_Ex22_C =>
fun x : Empty_set => match x return (SSN -> Salary) with
end
| FirstName_Ex22_C =>
fun x : Empty_set => match x return (FirstName -> Salary) with
end
| LastName_Ex22_C =>
fun x : Empty_set => match x return (LastName -> Salary) with
end
| Salary_Ex22_C =>
fun x : Empty_set => match x return (Salary -> Salary) with
end
| T1_Ex22_C =>
fun x : Empty_set =>
match x return (T1_Id_Ex222 -> Salary) with
end
| T2_Ex22_C =>
fun (_ : unit) (id : T2_Id_Ex222) =>
Salary_intro
match id with
| y1_Ex222 => 150
| y2_Ex222 => 200
| y3_Ex222 => 225
| y4_Ex222 => 200
end
end m0
| T1_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end ->
match c0 with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end -> T1_Id_Ex222)
with
| SSN_Ex22_C =>
fun x : Empty_set => match x return (SSN -> T1_Id_Ex222) with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match x return (FirstName -> T1_Id_Ex222) with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match x return (LastName -> T1_Id_Ex222) with
end
| Salary_Ex22_C =>
fun x : Empty_set =>
match x return (Salary -> T1_Id_Ex222) with
end
| T1_Ex22_C =>
fun x : Empty_set =>
match x return (T1_Id_Ex222 -> T1_Id_Ex222) with
end
| T2_Ex22_C =>
fun x : Empty_set =>
match x return (T2_Id_Ex222 -> T1_Id_Ex222) with
end
end m0
| T2_Ex22_C =>
fun
m0 : match s0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end =>
match
s0 as c0
return
(match c0 with
| SSN_Ex22_C => Empty_set
| FirstName_Ex22_C => Empty_set
| LastName_Ex22_C => Empty_set
| Salary_Ex22_C => Empty_set
| T1_Ex22_C => Empty_set
| T2_Ex22_C => Empty_set
end ->
match c0 with
| SSN_Ex22_C => SSN
| FirstName_Ex22_C => FirstName
| LastName_Ex22_C => LastName
| Salary_Ex22_C => Salary
| T1_Ex22_C => T1_Id_Ex222
| T2_Ex22_C => T2_Id_Ex222
end -> T2_Id_Ex222)
with
| SSN_Ex22_C =>
fun x : Empty_set => match x return (SSN -> T2_Id_Ex222) with
end
| FirstName_Ex22_C =>
fun x : Empty_set =>
match x return (FirstName -> T2_Id_Ex222) with
end
| LastName_Ex22_C =>
fun x : Empty_set =>
match x return (LastName -> T2_Id_Ex222) with
end
| Salary_Ex22_C =>
fun x : Empty_set =>
match x return (Salary -> T2_Id_Ex222) with
end
| T1_Ex22_C =>
fun x : Empty_set =>
match x return (T1_Id_Ex222 -> T2_Id_Ex222) with
end
| T2_Ex22_C =>
fun x : Empty_set =>
match x return (T2_Id_Ex222 -> T2_Id_Ex222) with
end
end m0
end m) g (S0 b c) = S0 b' c'}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment