update Truncations.v and PropositionalFracture.v for no funext