parsed in the context of the goal (so something like `f b` above will
> ensure that f and b get the right types rather than `’a->’b` and `’a`).
>
>
>
> Michael
>
>
>
> *From: *Haitao Zhang
> *Date: *Wednesday, 6 March 2019 at 18:42
> *To: *"Norrish,
ven’t shown us any assumptions/theorems about scr.)
Michael
From: Haitao Zhang mailto:zhtp...@gmail.com>>
Date: Wednesday, 6 March 2019 at 16:57
To: hol-info
mailto:hol-info@lists.sourceforge.net>>
Subject: [Hol-info] HOL difficulty with this subgoal
I had great difficulty to have
>>
>>sce A a = scr A c sce A a
>>
>>
>>
>> (You haven’t shown us any assumptions/theorems about scr.)
>>
>>
>>
>> Michael
>>
>>
>>
>> *From: *Haitao Zhang
>> *Date: *Wednesday, 6 March 2019 at 16:57
>> *To: *ho
scr.)
>
>
>
> Michael
>
>
>
> *From: *Haitao Zhang
> *Date: *Wednesday, 6 March 2019 at 16:57
> *To: *hol-info
> *Subject: *[Hol-info] HOL difficulty with this subgoal
>
>
>
> I had great difficulty to have HOL prove the following subgoal (I turned
> on typin
difficulty with this subgoal
I had great difficulty to have HOL prove the following subgoal (I turned on
typing for debugging, ``$c`` is a composition operator like ``$o``):
scf (A :mor -> bool) A (λ(x :mor). x) c sce A (a :mor) = scr A c sce A a
I had great difficulty to have HOL prove the following subgoal (I turned on
typing for debugging, ``$c`` is a composition operator like ``$o``):
scf (A :mor -> bool) A (λ(x :mor). x) c sce A (a :mor) = scr A c sce A a
0. homset (A :mor -> bool)
