through path type preservation
just a couple proofs left to prettify