inv image ind a: The basic lemma. Read this to understand proof method
inv image ind tp: A template proof for the InvImageInd tactic
inv_image_ind_tac: Definition of the InvImageInd tactic
rank_ind_tac: Definition of RankInd tactic.
Often more convenient than InvImageInd
inv image ind: Test of InvImageInd tactic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html