DEFINITION clt_wf_ind()
TYPE =
       P:CProp.(c:C.(d:C.(clt d c)(P d))(P c))c:C.(P c)
BODY =
Show proof