Add some missing internal validity and equivalence lemmas for dfrac, auth and agree

Ike Mulderrequested to merge
snyke7/iris:ike/internal_validity into master

Added some missing internal validity and equivalence lemmas for dfrac, auth and agree, which I used in !930 (closed).

Edited by Ike Mulder

Merge request reports