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.
|