TY - RPRT TI - Proof-irrelevant model of CC with predicative induction and judgmental equality AU - Gyesik Lee AU - Benjamin Werner PY - 2011 DO - 10.2168/lmcs-7(4:5)2011 UR - https://arxiv.org/abs/1111.0123 ID - 1111.0123 ER -