Theorem Tree_univalence (T1 T2 : Tree) : (T1 = T2) ≃ (Tree_iso T1 T2). Proof. set (P := λ G, λ H, TRRGraph_univalence G H). set (Q := λ G, (isatree G ,, isaprop_isatree G)). apply (substructure_univalence _ _ P Q T1 T2). Qed.