turns out: ind-cong is a special case of H.cong₂
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 5 Jan 2015 09:40:23 +0000 (10:40 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 5 Jan 2015 09:40:23 +0000 (10:40 +0100)
commitc5f982320394b5083e4ebca921c1cd5e88df9b14
treeb397cf1fb4ee697699fe59031c3203c68e46266b
parent69f47cad0ac14a7549e1e94b9f9a40f9935ad99e
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.
LiftGet.agda