#A; #B; #H; napply (fi … H); nassumption.
nqed.
-notation ". r" with precedence 50 for @{'fi $r}.
+notation ". r" with precedence 55 for @{'fi $r}.
interpretation "fi" 'fi r = (fi' ?? r).
ndefinition and_morphism: unary_morphism1 CPROP (unary_morphism1_setoid1 CPROP CPROP).
- x1...xn are bound in E and P, H is bound in P
- H is an identifier that will have the type of E in P
- P is the proof that the two existentially quantified predicates are equal*)
-notation > "∑ list1 ident x sep , . term 56 E / ident nE ; term 19 H" with precedence 20
+notation > "∑ list1 ident x sep , . term 61 E / ident nE ; term 19 H" with precedence 20
for @{ 'Sig_gen
${ fold right @{ 'End } rec acc @{ ('Next (λ${ident x}.${ident x}) $acc) } }
${ fold right @{ $E } rec acc @{ λ${ident x}.$acc } }
((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
#S m x y E; napply (.=_1 (∑w. E / E ; ((E ╪_1 #) ╪_1 #)) ╪_1 #). //; nqed.
*)
-
\ No newline at end of file
+