blob: 580cd87d1ead87e7e4171dfdf700e44381a13d3c (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* L'algo d'inférence du prédicat doit gérer le K-rédex dans le type de b *)
(* Problème rapporté par Solange Coupet *)
Section A.
Variables Alpha:Set; Beta:Set.
Definition nodep_prod_of_dep: (sigS Alpha [a:Alpha]Beta)-> Alpha*Beta:=
[c] Cases c of (existS a b)=>(a,b) end.
End A.
|
