fix: isRfl must ignore contextDependent; add unit tests

isRfl was using `matches .rfl` which only matched when ALL fields
have default values. With the new contextDependent field, .rfl false true
(cd=true) no longer matched, causing Theorems.rewrite to incorrectly
return cd .rfl results instead of continuing to the next theorem.

Fix: match `.rfl false _` (done=false, ignore cd).

Add unit tests for mkEqTransResult, andThen, orElse cd propagation.