proposition: Theorem Tree_univalence (T1 T2 : Tree) : (T1 = T2) ≃ (Tree_iso T1 T2).
proof: 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.
imports: UniMath.Foundations.PartB UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.HLevels UniMath.Combinatorics.WellOrderedSets UniMath.Combinatorics.OrderedSets UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions