diff options
| author | Helmut Grohne <grohne@cs.uni-bonn.de> | 2015-01-05 10:40:23 +0100 |
|---|---|---|
| committer | Helmut Grohne <grohne@cs.uni-bonn.de> | 2015-01-05 10:40:23 +0100 |
| commit | c5f982320394b5083e4ebca921c1cd5e88df9b14 (patch) | |
| tree | b397cf1fb4ee697699fe59031c3203c68e46266b /Bidir.agda | |
| parent | 69f47cad0ac14a7549e1e94b9f9a40f9935ad99e (diff) | |
| download | bidiragda-c5f982320394b5083e4ebca921c1cd5e88df9b14.tar.gz | |
turns out: ind-cong is a special case of H.cong₂
The major differences between them are:
* ind-cong treats the first parameter to the function implicit whereas
H.cong₂ makes it explicit.
* ind-cong expects a propositional proof for the first equality whereas
H.cong₂ asks for a heterogeneous one. Lift using H.reflexive.
Diffstat (limited to 'Bidir.agda')
0 files changed, 0 insertions, 0 deletions